functor Prfgen (S : PRFGEN_STRUCTS) : PRFGEN =
struct
  open S
  structure F = Frame
  structure A = Frame.Assem
  structure Coq = Coqize(structure Assem = A)
  structure Err = ErrorMsg
  structure T = Temp

  val localDebug = ref false
  fun dbpr s = if !localDebug
               then print (s^"\n")
               else ()

  val cbPrefix = "C_"
  val cbTpPrefix = "T_"
  val fchPostfix = "_fch"
  val preCondPrefix = "pre_"
  val postCondPrefix = "post_"
  val fctPostfix = "_fct"
  val chname = "ch"
  val ctname = "ct"
  val signame = "sg"

  val wfFblkPrefix = "WF_FBLK_"
  val wfFuncPrefix = "WF_FUNC_"
  val coqfilePostfix = "_asm.v"
  val cbFstPremiseName = "F0"
  val lemmaPrefix = "lemma_"
  val wfCH = "WF_CH"

  fun cbLemName lab = "CB_"^lab^"_wf"


  fun getSomethingFromFrame (frame, getSomething, errorMsg) =
      (case (getSomething frame)
        of  NONE => raise Fail errorMsg
          | SOME cl => cl)

  fun genLab framelist : string =
      let fun genf frame =
              let val codelist =
                      getSomethingFromFrame (frame, F.getCode, "no code, impossible")
                  fun f cb =
                      let val l = A.getCbLab cb
                      in  if l = "main"
                          then NONE
                          else SOME (l, A.getCbId cb)
                      end
                  val cblabl = List.mapPartial f codelist
              in  cblabl
              end
          val lib = [("print", 1), ("printp", 2), ("printb", 3)]
          val all = lib @ List.concat (List.map genf framelist)
          val labstr = String.concat (List.map Coq.ppLab all)
      in  "\n(* code label notation *)\n"^labstr^"\n"
      end

  fun genCodeHeap framelist : string =
      let fun genf frame : string =
              let val codelist = 
                      getSomethingFromFrame (frame, F.getCode, "no code, impossible")
                  fun gencb cb =
                      let val code = A.getCbCode cb
                          val name = A.getCbLab cb
                      in Coq.ppCodeBlock (cbPrefix^name, code)
                      end
                  val cblstr = String.concat (List.map gencb codelist)
                  val fname = (F.getFname frame)^fchPostfix
                  val f = fn cb => (A.getCbLab cb)
                  val lablist = List.map f codelist
                  val fchstr = Coq.ppFCodeHeap (fname, lablist, cbPrefix)
              in  cblstr ^ fchstr
              end     
          val fch = String.concat (List.map genf framelist)
          val g = fn fr => (F.getFname fr)
          val fnamelist = List.map g framelist
          val ch = Coq.ppCodeHeap (chname, fnamelist, fchPostfix)
      in  "\n(* code heap definition *)\n" ^ fch ^ ch
      end 

  fun andAsst (asst1, asst2) =
      fn s0 =>
      fn s1 => 
         A.And(asst1 s0 s1, asst2 s0 s1)

 fun completePreCond precond =
      let val extra = 
              let val newid1 = T.new_V "v"
                  val newid2 = T.new_V "v"                
                  val asst2 = 
                   fn s0 =>
                   fn s =>
                      A.Ex((newid1, A.Int), 
                           A.Eq(A.Sel(A.getHp s0, A.Sel(A.getRf s0, A.Reg(A.Esp))), 
                                A.Some (A.Id newid1)))
                  val asst3 = 
                   fn s0 =>
                   fn s =>
                      A.Ex((newid2, A.Int), 
                           A.Eq(A.Sel(A.getHp s0, A.Plus(A.Sel(A.getRf s0, A.Reg(A.Esp)), A.IntNum 4)), 
                                A.Some (A.Id newid2)))
                  val asst4 =
                   fn s0=>
                   fn s =>
                      A.Eq(A.State(s), A.State(s0))
              in  andAsst (asst2, (andAsst (asst3, asst4)))
              end
      in  andAsst(extra, precond)
      end

  fun completeAllCond (fstcond, size) =
      let val extra =
              let val newid1 = T.new_V "v"
                  val newid2 = T.new_V "v"
                  val asst1 = 
                   fn s0 =>
                   fn s => A.Stack (s, s0)
                  val asst4 = 
                   fn s0 =>
                   fn s =>
                      A.Eq(A.Sel(A.getHp s, A.Sel(A.getRf s, A.Reg(A.Ebp))), 
                           A.Some (A.Sel(A.getRf s0, A.Reg(A.Ebp))))
                  val asst5 =
                   fn s0 =>
                   fn s =>
                      A.Eq(A.Sel(A.getHp s, A.Minus (A.Sel(A.getRf s, A.Reg(A.Ebp))
                                                   , A.IntNum 4)), 
                           A.Some (A.Sel(A.getRf s0, A.Reg(A.Ebx))))
                  val asst6 =
                   fn s0 =>
                   fn s =>
                      A.Eq(A.Sel(A.getHp s, A.Minus (A.Minus (A.Sel(A.getRf s, A.Reg(A.Ebp))
                                                            , A.IntNum 4),
                                                     A.IntNum 4)), 
                           A.Some (A.Sel(A.getRf s0, A.Reg(A.Esi)))) 
                  val asst7 =
                   fn s0 =>
                   fn s =>
                      A.Eq(A.Sel(A.getHp s, A.Minus (A.Minus (A.Minus(A.Sel(A.getRf s, A.Reg(A.Ebp))
                                                                    , A.IntNum 4)
                                                            , A.IntNum 4)
                                                   , A.IntNum 4)), 
                           A.Some (A.Sel(A.getRf s0, A.Reg(A.Edi))))

                  val asst8 = 
                   fn s0 =>
                   fn s =>
                      A.Eq(A.Plus (A.Sel(A.getRf s, A.Reg(A.Ebp)), A.IntNum 4), A.Sel(A.getRf s0, A.Reg(A.Esp)))
                  val asst9 = 
                   fn s0 =>
                   fn s =>
                      A.Eq (A.Plus (A.Sel (A.getRf s, A.Reg A.Esp)
                                  , A.IntNum size)
                          , A.Sel(A.getRf s, A.Reg A.Ebp))
                  val asst2 = 
                   fn s0 =>
                   fn s =>
                      A.Ex((newid1, A.Int), 
                           A.Eq(A.Sel(A.getHp s0, A.Sel(A.getRf s0, A.Reg(A.Esp))), 
                                A.Some (A.Id newid1)))
                  val asst3 = 
                   fn s0 =>
                   fn s =>
                      A.Ex((newid2, A.Int), 
                           A.Eq(A.Sel(A.getHp s0, A.Plus(A.Sel(A.getRf s0, A.Reg(A.Esp)), A.IntNum 4)), 
                                A.Some (A.Id newid2)))

              in  andAsst 
                      (asst1, 
                       andAsst 
                           (asst2, 
                            andAsst 
                                (asst3, 
                                 andAsst 
                                     (asst4, 
                                      andAsst 
                                          (asst5, 
                                           andAsst 
                                               (asst6, 
                                                andAsst 
                                                    (asst7, 
                                                     andAsst 
                                                         (asst8, 
                                                          asst9))))))))
              end
      in  andAsst(extra, fstcond)
      end

  fun completePostCond postcond =
      let val extra =
              let val newid1 = T.new_V "v"
                  val newid2 = T.new_V "v"
                  val asst2 = 
                   fn s0 =>
                   fn s =>
                      A.Eq(A.Sel(A.getRf s0, A.Reg(A.Ebp)), A.Sel(A.getRf s, A.Reg(A.Ebp)))
                  val asst3 =
                   fn s0 =>
                   fn s =>
                      A.Eq(A.Sel(A.getRf s, A.Reg(A.Esp)), A.Plus(A.Sel(A.getRf s0, A.Reg(A.Esp)), A.IntNum 8))
                  val asst1 =
                   fn s0 =>
                   fn s =>
                      A.Stack(s, s0)
              in  andAsst(asst1, andAsst(asst2, asst3))
              end
      in  andAsst(extra, postcond)
      end

  fun justifyAsst framelist = 
      let fun justFrame frame = 
              let val (pre, prep) = 
                      getSomethingFromFrame (frame, F.getPre, "no precondition, impossible")
                  val newpre = completePreCond pre
                  val newframe1 = F.setPre(frame, SOME(newpre, prep))
                  val (post, postp) =
                      getSomethingFromFrame (newframe1, F.getPost, "no postcondition, impossible")
                  val newpost = completePostCond post
                  val newframe2 = F.setPost(newframe1, SOME(newpost, postp))
                  val codelist = 
                      getSomethingFromFrame (newframe2, F.getCode, "no code, impossible")
                  fun justCodeBlock size cb =
                      let val cblab = A.getCbLab cb
                          val fname = F.getFname newframe2
                          val newcb = 
                              case A.getCbAsst cb
                               of NONE => cb
                                | SOME p => if cblab = fname
                                            then A.setCbAsst (cb, completePreCond p)
                                            else A.setCbAsst (cb, completeAllCond (p, size))
                      in newcb
                      end
                  val size' = F.getLocals newframe2
                  val newcodelist = List.map (justCodeBlock size') codelist
                  val newframe3 = F.setCode(newframe2, newcodelist)
              in  newframe3
              end 
      in  List.map justFrame framelist
      end
  fun filtDot s = Coq.rpDot s
  fun genCodeHeapType framelist : string =
      let fun genf frame = 
              let val fname = F.getFname frame
                  val prename = preCondPrefix^ fname
                  fun asst2str (name, p) =
                      case p
                       of  NONE => (name ^" : no assertion\n") 
                         | SOME p => Coq.ppAsst (name, p) 
                  val prestr = asst2str (prename, F.getPreA frame)
                  val postname = postCondPrefix ^ fname
                  val poststr = asst2str (postname, F.getPostA frame)
                  val codelist = 
                      getSomethingFromFrame (frame, F.getCode, "no code, impossible")
                  val _ = dbpr "genCodeHeapType 1"
                  fun genCodeBlockType cb =
                      let val _ = dbpr "genCodeBlockType enter"
                          val ctname = cbTpPrefix ^ (filtDot (A.getCbLab cb))
                          val ctstr = 
                              case A.getCbAsst cb
                               of  NONE => (ctname ^ " : no assertion\n") 
                                 | SOME p => Coq.ppAsst (ctname, p) 
                          val _ = dbpr "genCodeHeapType : genCodeBlockType : 1"
                          val cbctl = A.getCbAlist cb
                          val _ = dbpr "genCodeHeapType : genCodeBlockType : 2"
                          fun cbct2str (name, asst) = 
                              let val name' = filtDot name
                                  val _ = dbpr ("genCodeHeapType : genCodeBlockType : cbct2str : now print assert : "^ name')
                                  val astr =Coq.ppAsst (name', asst)
                              in  dbpr ("genCodeHeapType : genCodeBlockType : cbct2str : print assert : "^ name'^ " finished")
                                ; astr
                              end
                          val ctstr2 = String.concat(List.map cbct2str cbctl)
                          val _ = dbpr ("genCodeHeapType : genCodeBlockType 3")
                      in ctstr ^ ctstr2
                      end
                  val ctliststr = String.concat (List.map genCodeBlockType codelist)
                  val _ = dbpr "genCodeHeapType 2"
                  val fctname = fname ^ fctPostfix
                  val f = fn cb => (A.getCbLab cb)
                  val lablist = List.map f codelist
                  val fctstr = Coq.ppFCodeHeapType (fctname, lablist, cbTpPrefix)
              in  prestr ^ poststr ^ ctliststr ^ fctstr
              end
          val liblist = ["print", "printp", "printb"]
          fun genFctlib libl =
              let val asst = fn s0 =>
                             fn s => A.True                  
                  fun prpre fname = Coq.ppAsst (preCondPrefix^fname, asst)
                  fun prpost fname = Coq.ppAsst (postCondPrefix^fname, asst)
                  val pre = String.concat (List.map prpre libl)
                  val post = String.concat (List.map prpost libl)
              in  pre ^ post
              end 
          val fctlib = genFctlib liblist
          val _ = dbpr fctlib
          val fct = (String.concat (List.map genf framelist))
          val g = fn fr => (F.getFname fr)
          val fnamelist = (List.map g framelist)
          val ch = Coq.ppCodeHeapType (ctname, fnamelist, fctPostfix)
          val sigma = Coq.ppSigma (signame, (liblist @ fnamelist), preCondPrefix, postCondPrefix)
      in  "\n(*code heap type definition *)\n" ^fctlib^ fct ^ ch ^ sigma
      end
      


  fun getFct frame =
      let val codelist = 
              getSomethingFromFrame (frame, F.getCode, "no code, impossible")
          fun get cb = (A.getCbLab cb, A.getCbAsst cb)
      in  List.map get codelist
      end

  fun getSigma framelist = 
      let val dumpa' = 
           fn S0 =>
           fn S => A.True
          val dumpa = SOME dumpa'
          val presigma = [("print", (dumpa, dumpa)), ("printb", (dumpa, dumpa)), ("printp", (dumpa, dumpa))]
          fun get frame = (F.getFname frame, (F.getPreA frame, F.getPostA frame))
      in  presigma @ (List.map get framelist)
      end

  fun getAsstFromCt (lab, cdhptp) : (A.assert option) = 
      let fun look [] = raise Fail "no such label"
            | look ((l, x) :: xs) =
              (dbpr ("getAsstFromCt : now look up "^ l ^" vs. "^ lab)
             ; if l = lab
               then x
               else look xs)
      in  look cdhptp
      end

  fun getPreFromSg (lab, sigma : (string * (A.assert option * A.assert option)) list) : (A.assert option) =
      let fun look [] = raise Fail "no such function"
            | look ((l, x : (A.assert option * A.assert option)) :: xs) =
              if l = lab
              then  (#1 x)
              else look xs
      in look sigma
      end

  fun getPostFromSg (lab, sigma : (string * (A.assert option * A.assert option)) list) : (A.assert option) =
      let fun look [] = raise Fail "no such function"
            | look ((l, x : (A.assert option * A.assert option)) :: xs) =
              if l = lab
              then (#2 x)
              else look xs
      in look sigma
      end

  fun getCode (lab, codelist) = 
      (case codelist
        of  [] => raise Fail "no code"
          | (c :: cl) =>
            if (A.getCbLab c) = lab
            then c
            else getCode (lab, cl))

  fun setCode (codelist, code) =
      (case codelist
        of  [] => []
          | (c :: cl) =>
            if (A.getCbLab c) = (A.getCbLab code)
            then code :: cl
            else c :: (setCode (cl, code)))

  fun wellJump (frame, sigma, l) = 
      let val _ = dbpr ("wellJump : " ^ l ^ " begin")
          val codelist = 
              getSomethingFromFrame (frame, F.getCode, "no code, impossible")
          val cdhptp = getFct frame 
          val code = getCode (l, codelist)
          val ins_rev = List.rev (A.getCbCode code)
          fun gen ins =
              (case ins
                of  ((A.Jmp l') :: is) =>
                    let val post = getAsstFromCt (l', cdhptp)
                        val _ = if !localDebug
                                then case (A.getCbAsst (getCode (l', codelist)))
                                      of  NONE => dbpr ("1 wellJump : "^l'^" : no postcond")
                                        | SOME a => dbpr ("1 wellJump : "^l'^" : has postcond") 
                                else ()
                    in case post
                        of  NONE => (dbpr ("2 wellJump : "^l'^" : no postcond")
                                   ; NONE)
                          | SOME p => (dbpr ("2 wellJump : "^l'^" : has postcond") 
                                     ; SOME (code, p, p))
                    end
                  | ((A.Jg (l, ln)) :: is) =>
                    let val post = getAsstFromCt (l, cdhptp)
                        val postn = getAsstFromCt (ln, cdhptp)
                    in case post
                        of NONE => NONE
                         | SOME p => (case postn 
                                       of  NONE => NONE
                                         | SOME pn => SOME (code, p, pn))
                    end
                  | ((A.Jge (l, ln)) :: is) =>
                    let val post = getAsstFromCt (l, cdhptp)
                        val postn = getAsstFromCt (ln, cdhptp)
                    in  case post
                         of  NONE => NONE
                           | SOME p => (case postn
                                         of  NONE => NONE
                                           | SOME pn => SOME (code, p, pn))
                    end
                  | ((A.Je (l, ln)) :: is) =>
                    let val post = getAsstFromCt (l, cdhptp)
                        val postn = getAsstFromCt (ln, cdhptp)
                    in case post
                        of NONE => NONE
                         | SOME p => (case postn 
                                       of  NONE => NONE
                                         | SOME pn => SOME (code, p, pn))
                    end
                  | ((A.Call (f, fret)) :: is) =>
                    let val post = getPreFromSg (f, sigma)
                        val postn = getAsstFromCt (fret, cdhptp) 
                    in  case post
                         of  NONE => NONE
                           | SOME p => (case postn
                                         of  NONE => NONE
                                           | SOME pn => SOME (code, p, pn))
                    end 
                  | (A.Ret(lb) :: is) =>
                    let val post = F.getPostA frame
                    in  case post
                         of  NONE => NONE
                           | SOME p => SOME (code, p, p)
                    end
                  | ((A.Malloc (i, l, t)) :: is) => 
                    let val post = getAsstFromCt (l, cdhptp)
                    in  case post
                         of  NONE => NONE
                           | SOME p => SOME (code, p, p)
                    end
                  | _ => raise Fail "last instruction should be JUMP instruction.")
      in  gen (ins_rev)
      end
 
 fun genNewAsst (instr, asst) : A.assert = 
      let 
	  fun rf(state:A.state) = A.getRf state
	  fun hp(state:A.state) = A.getHp state
	  fun mapGlobal str = 0

	  fun mchinstr (A.Addr (r1, r2)) s0 s = 
	      let val updexp2 = A.Plus(A.Sel(rf s, A.Reg r2),
				       A.Sel(rf s, A.Reg r1))
		  val s' = A.updRf (A.Upd(rf s, A.Reg r2, updexp2), s)
	      in  asst s0 s'
	      end
	    | mchinstr (A.Addz (imm, r2)) s0 s = 
	      let val updexp2 = A.Plus (A.Sel(rf s,A.Reg r2),
				        A.IntNum imm)
		  val s' = A.updRf(A.Upd(rf s, A.Reg r2, updexp2), s)
	      in asst s0 s'
	      end
            | mchinstr (A.Addm (imm, r1, r2)) s0 s =
              let val newid = T.new_V "v" 
                  val p = A.Eq (A.Sel(hp s, A.Plus (A.Sel(rf s, A.Reg r1), A.IntNum imm)), A.Some (A.Id newid))
                  val updexp2 = A.Plus (A.Sel(rf s, A.Reg r2), A.Id newid)
                  val s' = A.updRf (A.Upd(rf s, A.Reg r2, updexp2), s)
              in  A.Ex ((newid, A.Int), A.And (p, asst s0 s'))
              end
	    | mchinstr (A.Subr (r1, r2)) s0 s = 
	      let val updexp2 = A.Minus (A.Sel(rf s, A.Reg r2),
				         A.Sel(rf s, A.Reg r1))
		  val s' = A.updRf (A.Upd(rf s, A.Reg r2, updexp2), s)
	      in  asst s0 s'
	      end
	    | mchinstr (A.Subz (imm, r2)) s0 s = 
	      let val updexp2 = A.Minus (A.Sel(rf s, A.Reg r2),
				         A.IntNum imm)
		  val s' = A.updRf (A.Upd(rf s, A.Reg r2, updexp2), s)
	      in  asst s0 s'
	      end
            | mchinstr (A.Subm (imm, r1, r2)) s0 s =
              let val newid = T.new_V "v" 
                  val p = A.Eq (A.Sel (hp s, A.Plus (A.Sel (rf s, A.Reg r1), A.IntNum imm)), A.Some (A.Id newid))
                  val updexp2 =A.Minus (A.Sel (rf s, A.Reg r2), A.Id newid)
                  val s' = A.updRf (A.Upd (rf s, A.Reg r2, updexp2), s)
              in  A.Ex ((newid, A.Int), A.And (p, asst s0 s'))
              end
	    | mchinstr (A.Mulr(r1, r2)) s0 s = 
	      let val updexp2 = A.Times(A.Sel(rf s, A.Reg r2),
				        A.Sel(rf s, A.Reg r1))
		  val s' = A.updRf (A.Upd(rf s, A.Reg r2, updexp2), s)
	      in  asst s0 s'
	      end
	    | mchinstr (A.Mulz(imm, r2)) s0 s = 
	      let val updexp2 = A.Times(A.Sel(rf s, A.Reg r2),
				        A.IntNum imm)
		  val s' = A.updRf (A.Upd(rf s, A.Reg r2, updexp2), s)
	      in  asst s0 s'
	      end
            | mchinstr (A.Mulm (imm, r1, r2)) s0 s =
              let val newid = T.new_V "v" 
                  val p = A.Eq (A.Sel (hp s, A.Plus (A.Sel (rf s, A.Reg r1), A.IntNum imm)), A.Some (A.Id newid))
                  val updexp2 =A.Times (A.Sel (rf s, A.Reg r2), A.Id newid)
                  val s' = A.updRf (A.Upd (rf s, A.Reg r2, updexp2), s)
              in  A.Ex ((newid, A.Int), A.And (p, asst s0 s'))
              end
            | mchinstr (A.Movr(r1, r2)) s0 s = 
	      let val s' = A.updRf (A.Upd (rf s, A.Reg r2, A.Sel(rf s, A.Reg r1)), s)
	      in  asst s0 s'
	      end
	    | mchinstr (A.Movz(imm, r2, t)) s0 s = 
	      let val s' = A.updRf (A.Upd(rf s, A.Reg r2, A.IntNum imm), s)
	      in  asst s0 s'
	      end
	    | mchinstr (A.Movld(imm, r1, r2)) s0 s = 
	      let val newid = T.new_V "v" 
                  val updexp1 = A.Sel(hp s, A.Plus(A.Sel(rf s, A.Reg r1),
						   A.IntNum imm))
                  val p = A.Eq (updexp1, A.Some (A.Id newid))
		  val s' = A.updRf (A.Upd(rf s, A.Reg r2, A.Id newid), s)
	      in  A.Ex ((newid, A.Int), A.And (p, asst s0 s'))
	      end
	    | mchinstr (A.Movst(r1, imm, r2)) s0 s = 
	      let val updexp1 = A.Plus(A.Sel(rf s, A.Reg r2), A.IntNum imm)
		  val hp' = A.Upd(hp s, updexp1, A.Sel(rf s, A.Reg r1))
		  val s' = A.updHp (hp', s)
                  val p = A.InDomM (s, updexp1)
	      in  A.And (p, asst s0 s')
	      end
	    | mchinstr (A.Leal(lb, r1)) s0 s = 
	      let val lb' = mapGlobal lb
		  val s' = A.updRf(A.Upd(rf s, A.Reg r1, A.IntNum lb'), s)
	      in asst s0 s'
	      end
	    | mchinstr (A.Leab(imm, r1, r2)) s0 s = 
	      let val updexp1 = A.Plus(A.Sel(rf s, A.Reg r1), A.IntNum imm)
		  val s' = A.updRf(A.Upd(rf s, A.Reg r2, updexp1), s)
	      in asst s0 s'
	      end
	    | mchinstr (A.Xchg(r1, r2)) s0 s = 
	      let val s1 = A.updRf(A.Upd(rf s, A.Reg r2, A.Sel(rf s, A.Reg r1)), s)
		  val s' = A.updRf(A.Upd(rf s1, A.Reg r1, A.Sel(rf s, A.Reg r2)), s) 
	      in asst s0 s'
	      end
	    | mchinstr (A.Cmpr(r1, r2)) s0 s = 
	      let val prec1 = A.Eq(A.Sel(rf s, A.Reg r2), A.Sel(rf s, A.Reg r1))
		  val prec2 = A.Gt(A.Sel(rf s, A.Reg r2), A.Sel(rf s, A.Reg r1))
		  val prec3 = A.Lt(A.Sel(rf s, A.Reg r2), A.Sel(rf s, A.Reg r1))

		  val rs1' = A.updRf(A.Upd(rf s, A.Zf, A.IntNum 1), s)
		  val rs1 = A.updRf(A.Upd(rf rs1', A.Sf, A.IntNum 0), s)

		  val rs2' = A.updRf(A.Upd(rf s, A.Zf, A.IntNum 0), s)
		  val rs2 = A.updRf(A.Upd(rf rs2', A.Sf, A.IntNum 0), s)

		  val rs3' = A.updRf(A.Upd(rf s, A.Zf, A.IntNum 0), s)
		  val rs3 = A.updRf(A.Upd(rf rs3', A.Sf, A.IntNum 1), s)
	      in A.And(A.Imply(prec1, asst s0 rs1), A.And(A.Imply(prec2, asst s0 rs2), A.Imply(prec3, asst s0 rs3)))
	      end
	    | mchinstr (A.Cmpz(imm, r2)) s0 s = 
	      let val prec1 = A.Eq(A.Sel(rf s, A.Reg r2), A.IntNum(imm))
		  val prec2 = A.Gt(A.Sel(rf s, A.Reg r2), A.IntNum(imm))
		  val prec3 = A.Lt(A.Sel(rf s, A.Reg r2), A.IntNum(imm))

		  val rs1' = A.updRf(A.Upd(rf s, A.Zf, A.IntNum 1), s)
		  val rs1 = A.updRf(A.Upd(rf rs1', A.Sf, A.IntNum 0), s)

		  val rs2' = A.updRf(A.Upd(rf s, A.Zf, A.IntNum 0), s)
		  val rs2 = A.updRf(A.Upd(rf rs2', A.Sf, A.IntNum 0), s)

		  val rs3' = A.updRf(A.Upd(rf s, A.Zf, A.IntNum 0), s)
		  val rs3 = A.updRf(A.Upd(rf rs3', A.Sf, A.IntNum 1), s)
	      in A.And(A.Imply(prec1, asst s0 rs1), A.And(A.Imply(prec2, asst s0 rs2), A.Imply(prec3, asst s0 rs3)))
	      end
	    | mchinstr (A.Push r1) s0 s = 
	      let val sttop = A.Minus(A.Sel(rf s, A.Reg(A.Esp)), A.IntNum(4)) 
		  val nhp = A.Upd(hp s, sttop, A.Sel(rf s, A.Reg r1))

		  val nrf = A.Upd(rf s, A.Reg(A.Esp), sttop)
		  val s' = A.updSt({hp = nhp, rf = nrf}, s)
	      in asst s0 s'
	      end
	    | mchinstr (A.Pop r1) s0 s = 
	      let val newid = T.new_V "v" 
                  val p = A.Eq (A.Sel(hp s, A.Sel(rf s, A.Reg(A.Esp))), A.Some (A.Id newid))

		  val sttop = A.Plus(A.Sel(rf s, A.Reg(A.Esp)), A.IntNum(4))

		  val s1 = A.updRf(A.Upd(rf s, A.Reg(A.Esp), sttop), s)
		  val s' = A.updRf(A.Upd(rf s1, A.Reg(r1), A.Id(newid)), s)
              in  A.Ex ((newid, A.Int), A.And (p, asst s0 s'))
              end
	    | mchinstr (A.Leave) s0 s = 
	      let val newid = T.new_V "v" 
                  val p = A.Eq (A.Sel(hp s, A.Sel(rf s, A.Reg(A.Ebp))), A.Some (A.Id newid))

		  val sttop = A.Plus(A.Sel(rf s, A.Reg(A.Ebp)), A.IntNum(4))

		  val s1 = A.updRf(A.Upd(rf s, A.Reg(A.Esp), sttop), s)
		  val s' = A.updRf(A.Upd(rf s1, A.Reg(A.Ebp), A.Id(newid)), s)
              in  A.Ex ((newid, A.Int), A.And (p, asst s0 s'))
              end
	    | mchinstr (A.Free(r1)) s0 s = 
	      let val s' = A.updRf (A.Upd(rf s, A.Reg r1, A.IntNum 0), s)
	      in  asst s0 s'
	      end
	    | mchinstr (_) s0 st = raise Fail "should not happen\n"
      in mchinstr instr
      end

  fun genNewAsst2 (instr, asst1, asst2, sigma) : A.assert = 
      let fun rf(state:A.state) = A.getRf state
	  fun hp(state:A.state) = A.getHp state

	  fun mchinstr (A.Jmp(lb)) s0 s = asst1 s0 s
	    | mchinstr (A.Jg(lb1, lb2)) s0 s = 
	      let val zf' = A.Sel(rf s, A.Zf)
		  val sf' = A.Sel(rf s, A.Sf)
		  val tbrch_c = A.And(A.Eq(zf', A.IntNum(0)), A.Eq(sf', A.IntNum(0)))
		  val fbrch_c = A.Or(A.Eq(zf', A.IntNum(1)), A.Eq(sf', A.IntNum(1)))
	      in A.And(A.Imply(tbrch_c, asst1 s0 s), A.Imply(fbrch_c, asst2 s0 s))
	      end
	    | mchinstr (A.Je(lb1, lb2)) s0 s = 
	      let val zf' = A.Sel(rf s, A.Zf)
		  val tbrch_c = A.Eq(zf', A.IntNum(1))
		  val fbrch_c = A.Eq(zf', A.IntNum(0))
	      in A.And(A.Imply(tbrch_c, asst1 s0 s), A.Imply(fbrch_c, asst2 s0 s))
	      end
	    | mchinstr (A.Jge(lb1, lb2)) s0 s = 
	      let val sf' = A.Sel(rf s, A.Sf)
		  val tbrch_c = A.Eq(sf', A.IntNum(0))
		  val fbrch_c = A.Eq(sf', A.IntNum(1))
	      in A.And(A.Imply(tbrch_c, asst1 s0 s), A.Imply(fbrch_c, asst2 s0 s))
	      end
	    | mchinstr (A.Call(lb1, lb2)) s0 s = 
	      let fun fdPQ i1 ((i2, t)::r) = if i1 = i2
					     then t
					     else fdPQ i1 r
		    | fdPQ i1 [] = raise Fail ("cannot find P/Q of function "^lb1^"\n")
		  val (pfop, qfop) = fdPQ lb1 sigma
		  val (pf, qf) = let fun tFn NONE = raise Fail "Do not have assert\n"
				       | tFn (SOME(t)) = t
				 in (tFn(pfop), tFn(qfop))
				 end
		  val lb1' = filtDot lb1
		  val lb2' = filtDot lb2

		  val p1 = A.Ne(A.Id(lb1), A.Id("main"))

		  val s2_1 = A.updRf(A.Upd(rf s, A.Reg(A.Esp), A.Minus(A.Sel(rf s, A.Reg(A.Esp)), A.IntNum(8))), s)
		  val s2_2 = A.updHp(A.Upd(hp s2_1, A.Minus(A.Sel(rf s, A.Reg(A.Esp)), A.IntNum(4)), A.Id(lb1')), s2_1)
		  val s2_3 = A.updHp(A.Upd(hp s2_2, A.Minus(A.Sel(rf s, A.Reg(A.Esp)), A.IntNum(8)), A.Id(lb2')), s2_2)
		  val p2 = pf s2_3 s2_3

                  val i = T.new_si ()
                  val istr = Int.toString i
                  val newrf = "rf"^istr
                  val newhp = "hp"^istr
		  val p3' = (fn s' => A.Imply((qf s2_3 s'), (asst2 s0 s'))) (A.setSt {hp = A.Hp(i), rf = A.Rf(i)})
		  val p3 = A.Forall ((newrf, A.Str("regfile")),
				     A.Forall((newhp, A.Str("memory")), p3'))

	      in A.And(p2, p3)
	      end
	    | mchinstr (A.Ret(l)) s0 s =
	      let fun fdPQ i1 ((i2, t)::r) = if i1 = i2
					     then t
					     else fdPQ i1 r
		    | fdPQ i1 [] = raise Fail ("cannot find P/Q of function "^l^"\n")
		  val (pfop, qfop) = fdPQ l sigma
		  val (pf, qf) = let fun tFn NONE = raise Fail "Do not have assert\n"
				       | tFn (SOME(t)) = t
				 in (tFn(pfop), tFn(qfop))
				 end

		  val p1 = A.Eq(A.Id(l), A.Id("main"))

		  val s2_1 = A.updRf(A.Upd(rf s, A.Reg(A.Esp), A.Plus(A.Sel(rf s, A.Reg(A.Esp)), A.IntNum(8))), s)
		  val p2 = qf s0 s2_1

		  val p3_1 = A.Eq(A.Sel(rf s0, A.Reg(A.Esp)), A.Sel(rf s, A.Reg(A.Esp)))
		  val p3_2 = A.Eq(A.Sel(rf s0, A.Reg(A.Ebp)), A.Sel(rf s, A.Reg(A.Ebp)))
		  
		  val n_mlb = T.new_V "m"
		  val p3_3 = A.Forall((n_mlb, A.Int) 
				    , A.Imply(A.Ge(A.Id(n_mlb), A.Sel(rf s0, A.Reg(A.Esp)))
					    , A.Eq(A.Sel(hp s0, A.Id(n_mlb)), A.Sel(hp s, A.Id(n_mlb)))))
		  val p3 = A.And(p3_1, A.And(p3_2, p3_3))
		  val ret_main = A.And(p2, p3)

		  val s1_1' = A.updRf(A.Upd(rf s, A.Reg(A.Esp), A.Plus(A.Sel(rf s, A.Reg(A.Esp)), A.IntNum(8))), s) 
		  val p1' = qf s0 s1_1'

		  val n_flb = T.new_V "f"
		  val n_lret = T.new_V "lret"
		  val p2_1' = A.Ex((n_flb, A.Int), 
				   A.Ex((n_lret, A.Int), A.And(A.Eq(A.Sel(hp s, A.Plus(A.Sel(rf s, A.Reg(A.Esp)), A.IntNum(4))), 
								    A.Some(A.Id(n_flb))),
							       A.Eq(A.Sel(hp s, A.Sel(rf s, A.Reg(A.Esp))),
								    A.Some(A.Id(n_lret))))))
		  val p2_2' = A.Eq(A.Sel(rf s0, A.Reg(A.Esp)),
				   A.Sel(rf s, A.Reg(A.Esp)))
		  val p2_3' = A.Eq(A.Sel(rf s0, A.Reg(A.Ebp)),
				   A.Sel(rf s, A.Reg(A.Ebp)))

		  val p2_4' = A.Forall((n_mlb, A.Int) 
				     , A.Imply(A.Ge(A.Id(n_mlb), A.Sel(rf s0, A.Reg(A.Esp)))
					     , A.Eq(A.Sel(hp s0, A.Id(n_mlb)), A.Sel(hp s, A.Id(n_mlb)))))
		  val p2' = A.And(p2_1', A.And(p2_2', A.And(p2_3', p2_4')))
		  val p3' = A.Ne(A.Id(l), A.Id("main"))
		  val ret_non_main = A.And(p1', p2')
              in  if l = "main"
		  then ret_main 
		  else ret_non_main
              end
	    | mchinstr (A.Malloc(sz, lb, tp)) s0 s = 
	      let val n_jlb = T.new_V "j"
		  val n_llb = T.new_V "l"
                  val p1_1 = A.Forall((n_jlb, A.Int),
				      A.Imply(A.And(A.Ge (A.Id n_jlb, A.IntNum 0),
                                                    A.Lt (A.Id(n_jlb), A.TrForm ("nattoz", A.IntNum(sz)))),
					    A.NotInDomM(s, A.Plus(A.Id(n_llb), A.Times (A.Id(n_jlb), A.IntNum 4)))))
		  fun writeS (S, size, base) = 
                      let fun w off = 
                              if off = 0 
                              then (A.Upd (hp S, base, A.IntNum 0), base)
                              else if off > 0 
                              then let val (S', addr) = w (off-1)
                                       val newaddr = A.Plus (addr, A.IntNum 4)
                                   in  (A.Upd (S', newaddr, A.IntNum 0), newaddr)
                                   end
                              else raise Fail "offset can not be negtive."
                          val (newhp, _) = w (size-1)
                      in  newhp
                      end
                  val s1' = A.updHp(writeS (s, sz, A.Id n_llb), s)		   
		  val s1 = A.updRf(A.Upd(rf s1', A.Reg(A.Eax), A.Id(n_llb)), s1')  
		  val p1_2 = asst2 s0 s1

		  val p1 = A.Forall((n_llb, A.Str("loc")), A.Imply(p1_1, p1_2))
	      in   p1
	      end
	    | mchinstr _ s0 s = raise Fail "bug\n"
      in mchinstr instr
      end

  fun genCbPf (fname, sigma, code, asst1 : A.assert, asst2 : A.assert) =
      let val ins_rev = List.rev (A.getCbCode code)
          val tagname = case (List.hd ins_rev) 
                         of (A.Ret fname) => fname^"_ret"
                          | _ => ""
          val _ = T.reset_asst()
          fun gen (ins, (pf, cb), code) =
              (case ins
                of  ((A.Jmp l) :: is) =>
                    let val post = asst1
                        val pre = post
                        val postname = cbTpPrefix ^ (filtDot l)
                        val lab = A.getCbLab code
                        val _ = dbpr ("now generating assertion of codeblock" ^ lab)
                    in  case is
                         of  [] => 
                             let val (newcode, tag) = 
                                     case (A.getCbAsst code)
                                      of  NONE => (A.setCbAsst (code, pre), "")
                                        | SOME a => let val newasst = T.new_asst lab
                                                        val newcode = A.addCbAlist (code, (newasst, pre))
                                                    in  (newcode, lab)
                                                    end
                                 val prf = A.WfJmp (postname, (A.Jmp l))
                                 val _ = if !localDebug
                                         then case (A.getCbAsst newcode) 
                                               of  NONE => dbpr ("genCbPf :" ^lab ^ "'s assertion is NONE")
                                                 | SOME a =>  dbpr ("genCbPf :" ^lab ^ "'s assertion is SOME")
                                         else ()
                             in  A.setCbPf (newcode, prf, tag)
                             end
                           | _ => 
                             let val newasst = T.new_asst lab 
                                 val newcode = A.addCbAlist (code, (newasst, pre))
                                 val newpf = A.WfJmp (postname, (A.Jmp l))
                                 val newcb = [A.Jmp l] 
                             in  gen (is, (newpf, newcb), newcode)
                             end 
                    end
                  | ((A.Jg (l, ln)) :: is) =>
                    let val post = asst1
                        val postn = asst2
                        val postname = cbTpPrefix ^ (filtDot l)
                        val postnname = cbTpPrefix ^ (filtDot ln)
                        val pre = genNewAsst2 (A.Jg (l, ln), post, postn, sigma) 
                        val lab = A.getCbLab code 
                    in  case is
                         of  [] =>
                             let val (newcode, tag) =
                                     case (A.getCbAsst code)
                                      of  NONE => (A.setCbAsst (code, pre), "")
                                        | SOME a => let val newasst = T.new_asst lab
                                                        val newcode = A.addCbAlist (code, (newasst, pre))
                                                    in  (newcode, lab)
                                                    end
                                 val prf = A.WfJg (postname, postnname, A.Jg (l, ln))
                             in  A.setCbPf (newcode, prf, tag) 
                             end
                           | _ =>
                             let val newasst = T.new_asst lab
                                 val newcode = A.addCbAlist (code, (newasst, pre))
                                 val newpf = A.WfJg (postname, postnname, A.Jg (l, ln))
                                 val newcb = [A.Jg (l, ln)]
                             in  gen (is, (newpf, newcb), newcode)
                             end
                    end
                  | ((A.Jge (l, ln)) :: is) =>
                    let val post = asst1
                        val postn = asst2
                        val postname = cbTpPrefix ^ (filtDot l)
                        val postnname = cbTpPrefix ^ (filtDot ln)
                        val pre = genNewAsst2 (A.Jge (l, ln), post, postn, sigma) 
                        val lab = A.getCbLab code 
                    in  case is
                         of  [] =>
                             let val (newcode, tag) =
                                     case (A.getCbAsst code)
                                      of  NONE => (A.setCbAsst (code, pre), "")
                                        | SOME a => let val newasst = T.new_asst lab
                                                        val newcode = A.addCbAlist (code, (newasst, pre))
                                                    in  (newcode, lab)
                                                    end
                                 val prf = A.WfJge (postname, postnname, A.Jge (l, ln))
                             in  A.setCbPf (newcode, prf, tag) 
                             end
                           | _ =>
                             let val newasst = T.new_asst lab
                                 val newcode = A.addCbAlist (code, (newasst, pre))
                                 val newpf = A.WfJge (postname, postnname, A.Jge (l, ln))
                                 val newcb = [A.Jge (l, ln)]
                             in  gen (is, (newpf, newcb), newcode)
                             end
                    end
                  | ((A.Je (l, ln)) :: is) =>
                    let val post = asst1
                        val postn = asst2
                        val postname = cbTpPrefix ^ (filtDot l)
                        val postnname = cbTpPrefix ^ (filtDot ln)
                        val pre = genNewAsst2 (A.Je (l, ln), post, postn, sigma) 
                        val lab = A.getCbLab code 
                    in  case is
                         of  [] =>
                             let val (newcode, tag) =
                                     case (A.getCbAsst code)
                                      of  NONE => (A.setCbAsst (code, pre), "")
                                        | SOME a => let val newasst = T.new_asst lab
                                                        val newcode = A.addCbAlist (code, (newasst, pre))
                                                    in  (newcode, lab)
                                                    end
                                 val prf = A.WfJe (postname, postnname, A.Je (l, ln))
                             in  A.setCbPf (newcode, prf, tag) 
                             end
                           | _ =>
                             let val newasst = T.new_asst lab
                                 val newcode = A.addCbAlist (code, (newasst, pre))
                                 val newpf = A.WfJe (postname, postnname, A.Je (l, ln))
                                 val newcb = [A.Je (l, ln)]
                             in  gen (is, (newpf, newcb), newcode)
                             end
                    end
                  | ((A.Malloc (i, l, t)) :: is) =>
                    let val post = asst1
                        val postname = cbTpPrefix ^ (filtDot l)
                        val pre = genNewAsst2 (A.Malloc (i, l, t), post, post, sigma) 
                        val lab = A.getCbLab code 
                    in  case is
                         of  [] =>
                             let val (newcode, tag) =
                                     case (A.getCbAsst code)
                                      of  NONE => (A.setCbAsst (code, pre), "")
                                        | SOME a => let val newasst = T.new_asst lab
                                                        val newcode = A.addCbAlist (code, (newasst, pre))
                                                    in  (newcode, lab)
                                                    end
                                 val _ = dbpr "enter A.Malloc"
                                 val prf = A.WfMalloc (postname, A.Malloc (i, l, t))
                             in  A.setCbPf (newcode, prf, tag) 
                             end
                           | _ =>
                             let val newasst = T.new_asst lab
                                 val newcode = A.addCbAlist (code, (newasst, pre))
                                 val newpf = A.WfMalloc (postname, A.Malloc (i, l, t))
                                 val newcb = [A.Malloc (i, l, t)]
                             in  gen (is, (newpf, newcb), newcode)
                             end
                    end
                  | (A.Ret(lb) :: is) =>
                    let val post = asst1
                        val postname = postCondPrefix ^ (filtDot fname)
                        val pre = genNewAsst2 (A.Ret(lb), post, post, sigma) 
                        val lab = A.getCbLab code 
                    in  case is
                         of  [] =>
                             let val (newcode, tag) =
                                     case (A.getCbAsst code)
                                      of  NONE => (A.setCbAsst (code, pre), "")
                                        | SOME a => let val newasst = T.new_asst lab
                                                        val newcode = A.addCbAlist (code, (newasst, pre))
                                                    in  (newcode, lab)
                                                    end
                                 val prf = A.WfRet (postname)
                             in  A.setCbPf (newcode, prf, tag) 
                             end
                           | _ =>
                             let val newasst = T.new_asst lab
                                 val newcode = A.addCbAlist (code, (newasst, pre))
                                 val newpf = A.WfRet (postname)
                                 val newcb = [A.Ret(lb)]
                             in  gen (is, (newpf, newcb), newcode)
                             end
                    end
                  | ((A.Call (f, fret)) :: is) =>
                    let val post = asst1
                        val postn = asst2 
                        val postname = cbTpPrefix ^ (filtDot f)
                        val postnname = cbTpPrefix ^ (filtDot fret)
                        val pre = genNewAsst2 (A.Call (f, fret), post, postn, sigma)
                        val lab = A.getCbLab code 
                    in  case is
                         of  [] =>
                             let val (newcode, tag) =
                                     case (A.getCbAsst code)
                                      of  NONE => (A.setCbAsst (code, pre), "")
                                        | SOME a => let val newasst = T.new_asst lab
                                                        val newcode = A.addCbAlist (code, (newasst, pre))
                                                    in  (newcode, lab)
                                                    end
                                 val prf = A.WfCall (postname, postnname, A.Call (f, fret))
                             in  A.setCbPf (newcode, prf, tag) 
                             end
                           | _ =>
                             let val newasst = T.new_asst lab
                                 val newcode = A.addCbAlist (code, (newasst, pre))
                                 val newpf = A.WfCall (postname, postnname, A.Call (f, fret))
                                 val newcb = [A.Call (f, fret)]
                             in  gen (is, (newpf, newcb), newcode)
                             end
                    end 
                  | ((A.Directive s) :: is) => (raise Fail "Directive should not appear in  code block")
                  | ((A.Section s) :: is) => (raise Fail "Section should not appear in  code block")
                  | ((A.Label (_, _)) :: is) => (raise Fail "Label should not appear in  code block")
                  | ((A.ExtrA a) :: is) => (* WIP *)
                    let val (postname, post) = A.getCbFstA code
                        val pre = post 
                        val lab = A.getCbLab code
                    in  case is
                         of  [] =>
                             let val (newcode, tag) =
                                     case (A.getCbAsst) code
                                      of  NONE => (A.setCbAsst (code, pre), "")
                                        | SOME a => (code, lab)
                             in  A.setCbPf (newcode, pf, tag)
                             end
                           | _ => gen (is, (pf, cb), code)
                    end
                  | (i :: is) =>
                    let val (postname', post) = A.getCbFstA code
                        val postname = filtDot postname'
                        val _ = dbpr (postname^" : "^(A.toString i)^"\n")
                        val pre = genNewAsst (i, post)
                        val lab = A.getCbLab code
                    in  case is
                         of  [] =>
                             let val (newcode, tag) =
                                     case (A.getCbAsst code)
                                      of  NONE => (A.setCbAsst (code, pre), "")
                                        | SOME a => let val newasst = T.new_asst lab
                                                        val newcode = A.addCbAlist (code, (newasst, pre))
                                                        val newlab = if tagname = "" 
                                                                     then lab
                                                                     else tagname 
                                                    in  (newcode, newlab)
                                                    end
                                 val prf = A.WfSeq (pf, postname, i :: cb)
                             in  A.setCbPf (newcode, prf, tag)
                             end
                           | _ =>
                             let val newasst = T.new_asst lab
                                 val newcode = A.addCbAlist (code, (newasst, pre))
                                 val newcb =  (i :: cb)
                                 val newpf = A.WfSeq (pf, postname, newcb)
                             in  gen (is, (newpf, newcb), newcode)
                             end
                    end
                  | [] => raise Fail "instruction sequence should not be empty. " )
      in  gen (ins_rev, (A.WfRet "bogus", []), code) 
      end 

  fun genFunPf (frame, sigma) =
      let val codelist = 
              getSomethingFromFrame (frame, F.getCode, "no code, impossible")
          val lablist = List.map (A.getCbLab) codelist
          val fname = F.getFname frame
          val _ = dbpr "genFunPf1"
          fun gen ([], fr) = fr
            | gen (l :: ls, fr) =
              let val welljump = wellJump (fr, sigma, l) 
              in  case welljump
                   of SOME (code, a1, a2) =>
                      let val newCode = genCbPf (fname, sigma, code, a1, a2)
                          val codelist' = getSomethingFromFrame (fr, F.getCode, "no code, impossible")
                          val newCodeList = setCode (codelist', newCode)
                          val newfr = F.setCode (fr, newCodeList)
                          val _ = dbpr ("genFunPf: codeblock "^ l ^" begin")
                          val _ = if !localDebug
                                  then let val codelist = 
                                               case (F.getCode newfr)
                                                of  NONE => raise Fail "can not find codelist in frame"
                                                  | SOME c => c
                                           val _ = (case (A.getCbAsst newCode)
                                                      of  NONE => dbpr ("1 genFunPf : " ^ l ^ " is still no assertion")
                                                        | SOME a => dbpr ("1 genFunPf : " ^ l ^ " has assertion"))
                                           val _ = (case (A.getCbAsst (getCode (l, newCodeList)))
                                                     of  NONE => dbpr ("2 genFunPf : " ^ l ^ " is still no assertion")
                                                       | SOME a => dbpr ("2 genFunPf : " ^ l ^ " has assertion"))
                                           val _ = (case (A.getCbAsst (getCode (l, codelist)))
                                                     of  NONE => dbpr ("3 genFunPf : " ^ l ^ " is still no assertion")
                                                       | SOME a => dbpr ("3 genFunPf : " ^ l ^ " has assertion"))
                                       in  ()
                                       end
                                  else ()
                      in  gen (ls, newfr)
                      end
                    | NONE => (dbpr ("genFunPf: codeblok "^ l ^ " is delayed"); gen (ls @ [l], fr))
              end
      in  gen (lablist, frame)
      end

  fun genProgPf framelist = 
      let val sigma = getSigma framelist
          val _ = dbpr "genProgPf1"
         
          fun f fr = genFunPf (fr, sigma)
          val fl = List.map f framelist
      in  dbpr "genProgPf2"
        ; fl
      end

  fun genWfCbLem (fname, cb) =
      let val lab = A.getCbLab cb
      in  Coq.ppCbLem (fname, lab, cbLemName, ctname, fctPostfix, signame, cbTpPrefix, cbPrefix)
      end

  fun genSubpf (precond : string, precond2 : string, na' : string, i : A.instr, tag : string) : A.tactic list = (* WIP *)
      (case i
        of (A.Addr (r1, r2)) => 
           let val tmpvar = T.new_var()
               val alist = ["S0", "S", tmpvar]
               val alist2 = [A.O "hp0", A.O "rf0"]
               val alist3 = [A.O "hp1", A.O"rf1"]
               val updexp2 = A.Plus (A.Sel(A.Rf 1, A.Reg r2),
				     A.Sel(A.Rf 1, A.Reg r1))
	       val rf = A.Upd (A.Rf 1, A.Reg r2, updexp2)
               val first =
                   [A.Tseq [A.Tintros alist
                          , A.Tinduction ("S0", alist2)
                          , A.Tinduction ("S", alist3)]
                  , A.TexistsS (A.Hp 1, rf)
                  , A.Tseq [A.Tsplit
                          , A.Tpara [A.Tconstructor
                                   , A.Tapply (tmpvar, [])
                                     
                   ]]]
           in  first
           end
         | (A.Xchg (r1, r2)) => 
           let val tmpvar = T.new_var()
               val alist = ["S0", "S", tmpvar]
               val alist2 = [A.O "hp0", A.O "rf0"]
               val alist3 = [A.O "hp1", A.O"rf1"]
               val rf' = A.Upd (A.Rf 1, A.Reg r2, A.Sel(A.Rf 1, A.Reg r1))
	       val rf = A.Upd (rf', A.Reg r1, A.Sel(A.Rf 1, A.Reg r2))
               val first =
                   [A.Tseq [A.Tintros alist
                          , A.Tinduction ("S0", alist2)
                          , A.Tinduction ("S", alist3)]
                  , A.TexistsS (A.Hp 1, rf)
                  , A.Tseq [A.Tsplit
                          , A.Tpara [A.Tconstructor
                                   , A.Tapply (tmpvar, [])
                   ]]]
           in  first
           end
         | (A.Push r) =>
           let val tmpvar = T.new_var ()
               val alist = ["S0", "S", tmpvar]
               val alist2 = [A.O "hp0", A.O "rf0"]
               val alist3 = [A.O "hp1", A.O"rf1"]
	       val rftop = A.Minus(A.Sel(A.Rf 1, A.Reg(A.Esp)), A.IntNum(4))                           
	       val hp = A.Upd(A.Hp 1, rftop, A.Sel(A.Rf 1, A.Reg r))
	       val rf = A.Upd(A.Rf 1, A.Reg A.Esp, rftop)
               val first = if tag = ""
                           then [A.Tseq [A.Tintros alist
                                       , A.Tinduction ("S0", alist2)
                                       , A.Tinduction ("S", alist3)]
                               , A.TexistsS (hp, rf)
                               , A.Tsplit
                               , A.Tconstructor
                               , A.Tapply (tmpvar, [])]
                           else let val tmpvar2 = T.new_var ()
                                    val tmpvar3 = T.new_var ()
                                    val tmpvar4 = T.new_var ()
                                    val tmpvar5 = T.new_var ()
                                    val tmpvar6 = T.new_var ()
                                    val tmpvar7 = T.new_var ()
                                    val tmpx = T.new_var ()
                                    val alist4 = [A.L [A.O tmpvar2
                                                     , A.L [A.O tmpvar3
                                                          , A.O tmpvar4]]
                                                , A.O tmpvar]
                                    val alist5 = [tmpvar5, tmpvar6]
                                    val alist6 = [tmpx, tmpvar7]
                                    val loc1 = A.Minus (A.Sel (A.Rf 0, A.Reg A.Esp), A.IntNum 4)
                                    val loc2 = A.Minus (loc1, A.IntNum 4)
                                    val loc3 = A.Minus (loc2, A.IntNum 4)
                                    val loc4 = A.Minus (loc3, A.IntNum 4)
                                    val v1 = A.Sel (A.Rf 0, A.Reg A.Ebp)
                                    val v2 = A.Sel (A.Rf 0, A.Reg A.Ebx)
                                    val v3 = A.Sel (A.Rf 0, A.Reg A.Esi)
                                    val v4 = A.Sel (A.Rf 0, A.Reg A.Edi)
                                    val hp1 = A.Upd (A.Hp 0, loc1, v1)
                                    val hp2 = A.Upd (hp1, loc2, v2)
                                    val hp3 = A.Upd (hp2, loc3, v3)
                                    val hp4 = A.Upd (hp3, loc4, v4)
                                    val exp1 = A.Sel (hp4, A.Id tmpx)
                                    val exp2 = A.Sel (hp3, A.Id tmpx)
                                    val exp3 = A.Sel (hp2, A.Id tmpx)
                                    val exp4 = A.Sel (hp1, A.Id tmpx)

                                    val exp1' = A.Sel (hp4, loc1)
                                    val exp2' = A.Sel (hp3, loc1)
                                    val exp3' = A.Sel (hp2, loc1)
                                    val exp4' = A.Sel (hp1, loc1)

                                    val exp1'' = A.Sel (hp4, loc2)
                                    val exp2'' = A.Sel (hp3, loc2)
                                    val exp3'' = A.Sel (hp2, loc2)
                                   
                                    val exp1''' = A.Sel (hp4, loc3)
                                    val exp2''' = A.Sel (hp3, loc3)

                                    val tmpvar8 = T.new_var ()
                                    val lemName = lemmaPrefix ^(filtDot tag) 
                                in  [A.Tintros alist
                                   , A.Tcut (precond2 ^ " S0 S")
                                   , A.Tintros [tmpvar2]
                                   , A.Tseq [A.Tinduction ("S0", alist2)
                                           , A.Tinduction ("S", alist3)]
                                   , A.TexistsS (hp, rf)
                                   , A.Tsplit
                                   , A.Tconstructor
                                   , A.Tapply (tmpvar2, [])
                                   , A.Tapply (lemName, [])
                                   , A.Tapply (tmpvar, [])
                                   ]
                                end
           in  first
           end
         | (A.Pop r) =>
           let val tmpvar = T.new_var ()
               val tmpvar2 = T.new_var ()
               val tmpvar3 = T.new_var ()
               val alist = ["S0", "S", tmpvar]
               val alist2 = [A.O "hp0", A.O "rf0"]
               val alist3 = [A.O "hp1", A.O"rf1"]
               val alist4 = [A.O tmpvar2, A.L [A.O tmpvar, A.O tmpvar3]]
	       val rftop = A.Plus(A.Sel(A.Rf 1, A.Reg(A.Esp)), A.IntNum(4))                           
	       val rf' = A.Upd(A.Rf 1, A.Reg(A.Esp), rftop)
	       val rf = A.Upd(rf', A.Reg(r), A.Id(tmpvar2))
               val first = [A.Tseq [A.Tintros alist
                                  , A.Tinduction ("S0", alist2)
                                  , A.Tinduction ("S", alist3)]
                          , A.Tdestruct (tmpvar, alist4)
                          , A.TexistsS (A.Hp 1, rf)
                          , A.Tseq [A.Tsplit
                                  , A.Tpara [A.Tseq [A.Tconstructor
                                                   , A.Tapply (tmpvar, [])]
                                           , A.Tapply (tmpvar3, [])
                           ]]]
           in  first
           end
         | (A.Movr (r1, r2))=>
           let val tmpvar = T.new_var ()
               val alist = ["S0", "S", tmpvar]
               val alist2 = [A.O "hp0", A.O "rf0"]
               val alist3 = [A.O "hp1", A.O"rf1"]
	       val rf = A.Upd (A.Rf 1, A.Reg r2, A.Sel(A.Rf 1, A.Reg r1))
               val first = [A.Tseq [A.Tintros alist
                                  , A.Tinduction ("S0", alist2)
                                  , A.Tinduction ("S", alist3)]
                          , A.TexistsS (A.Hp 1, rf)
                          , A.Tseq [A.Tsplit
                                  , A.Tpara [A.Tconstructor
                                           , A.Tapply (tmpvar, [])
                           ]]]
           in  first
           end
         | (A.Movz (i, r, t)) =>
           let val tmpvar = T.new_var ()
               val alist = ["S0", "S", tmpvar]
               val alist2 = [A.O "hp0", A.O "rf0"]
               val alist3 = [A.O "hp1", A.O"rf1"]
               val rf = A.Upd (A.Rf 1, A.Reg r, A.IntNum i)
               val first = [A.Tseq [A.Tintros alist
                                  , A.Tinduction ("S0", alist2)
                                  , A.Tinduction ("S", alist3)]
                          , A.TexistsS (A.Hp 1, rf)
                          , A.Tseq [A.Tsplit
                                  , A.Tpara [A.Tconstructor
                                           , A.Tapply (tmpvar, [])
                           ]]]
           in  first
           end
         | (A.Movld (i, r1, r2)) =>
           let val tmpvar = T.new_var ()
               val tmpvar2 = T.new_var ()
               val tmpx = T.new_var ()
               val alist = ["S0", "S", tmpvar]
               val alist2 = [A.O "hp0", A.O "rf0"]
               val alist3 = [A.O "hp1", A.O"rf1"]
               val alist4 = [A.O tmpx, A.L [A.O tmpvar, A.O tmpvar2]]
               val rf = A.Upd(A.Rf 1, A.Reg r2, A.Id tmpx)
               val first = [A.Tseq [A.Tintros alist
                                  , A.Tinduction ("S0", alist2)
                                  , A.Tinduction ("S", alist3)]
                          , A.Tdestruct (tmpvar, alist4)
                          , A.TexistsS (A.Hp 1, rf)
                          , A.Tseq [A.Tsplit
                                  , A.Tpara [A.Tseq [A.Tconstructor
                                                   , A.Tapply (tmpvar, [])]
                                           , A.Tapply (tmpvar2, [])
                           ]]]
           in  first
           end
         | (A.Movst (r1, i, r2)) =>
           let val tmpvar = T.new_var ()
               val tmpvar2 = T.new_var ()
               val tmpx = T.new_var ()
               val alist = ["S0", "S", tmpvar]
               val alist2 = [A.O "hp0", A.O "rf0"]
               val alist3 = [A.O "hp1", A.O"rf1"]
               val alist4 = [A.O tmpvar, A.O tmpvar2]
               val updexp1 =  A.Plus(A.Sel(A.Rf 1, A.Reg r2), A.IntNum i)
               val hp = A.Upd(A.Hp 1, updexp1, A.Sel (A.Rf 1, A.Reg r1))
               val first = [A.Tseq [A.Tintros alist
                                  , A.Tinduction ("S0", alist2)
                                  , A.Tinduction ("S", alist3)]
                          , A.Tdestruct (tmpvar, alist4)
                          , A.TexistsS (hp, A.Rf 1)
                          , A.Tseq [A.Tsplit
                                  , A.Tpara [A.Tseq [A.Tconstructor
                                                   , A.Tapply (tmpvar, [])]
                                           , A.Tapply (tmpvar2, [])
                           ]]]
           in  first
           end
         | (A.Addm (i, r1, r2)) =>
           let val tmpvar = T.new_var ()
               val tmpvar2 = T.new_var ()
               val tmpx = T.new_var ()
               val alist = ["S0", "S", tmpvar]
               val alist2 = [A.O "hp0", A.O "rf0"]
               val alist3 = [A.O "hp1", A.O"rf1"]
               val alist4 = [A.O tmpx, A.L [A.O tmpvar, A.O tmpvar2]]
               val updexp2 = A.Plus (A.Sel (A.Rf 1, A.Reg r2), A.Id tmpx)
               val rf = A.Upd(A.Rf 1, A.Reg r2, updexp2)
               val first = [A.Tseq [A.Tintros alist
                                  , A.Tinduction ("S0", alist2)
                                  , A.Tinduction ("S", alist3)]
                          , A.Tdestruct (tmpvar, alist4)
                          , A.TexistsS (A.Hp 1, rf)
                          , A.Tseq [A.Tsplit
                                  , A.Tpara [A.Tseq [A.Tconstructor
                                                   , A.Tapply (tmpvar, [])]
                                           , A.Tapply (tmpvar2, [])
                           ]]]
           in  first
           end
         | (A.Subm (i, r1, r2)) =>
           let val tmpvar = T.new_var ()
               val tmpvar2 = T.new_var ()
               val tmpx = T.new_var ()
               val alist = ["S0", "S", tmpvar]
               val alist2 = [A.O "hp0", A.O "rf0"]
               val alist3 = [A.O "hp1", A.O"rf1"]
               val alist4 = [A.O tmpx, A.L [A.O tmpvar, A.O tmpvar2]]
               val updexp2 = A.Minus (A.Sel (A.Rf 1, A.Reg r2), A.Id tmpx)
               val rf = A.Upd(A.Rf 1, A.Reg r2, updexp2)
               val first = [A.Tseq [A.Tintros alist
                                  , A.Tinduction ("S0", alist2)
                                  , A.Tinduction ("S", alist3)]
                          , A.Tdestruct (tmpvar, alist4)
                          , A.TexistsS (A.Hp 1, rf)
                          , A.Tseq [A.Tsplit
                                  , A.Tpara [A.Tseq [A.Tconstructor
                                                   , A.Tapply (tmpvar, [])]
                                           , A.Tapply (tmpvar2, [])
                           ]]]
           in  first
           end
         | (A.Mulm (i, r1, r2)) =>
           let val tmpvar = T.new_var ()
               val tmpvar2 = T.new_var ()
               val tmpx = T.new_var ()
               val alist = ["S0", "S", tmpvar]
               val alist2 = [A.O "hp0", A.O "rf0"]
               val alist3 = [A.O "hp1", A.O"rf1"]
               val alist4 = [A.O tmpx, A.L [A.O tmpvar, A.O tmpvar2]]
               val updexp2 = A.Times (A.Sel (A.Rf 1, A.Reg r2), A.Id tmpx)
               val rf = A.Upd(A.Rf 1, A.Reg r2, updexp2)
               val first = [A.Tseq [A.Tintros alist
                                  , A.Tinduction ("S0", alist2)
                                  , A.Tinduction ("S", alist3)]
                          , A.Tdestruct (tmpvar, alist4)
                          , A.TexistsS (A.Hp 1, rf)
                          , A.Tseq [A.Tsplit
                                  , A.Tpara [A.Tseq [A.Tconstructor
                                                   , A.Tapply (tmpvar, [])]
                                           , A.Tapply (tmpvar2, [])
                           ]]]
           in  first
           end
         | (A.Subz (i, r)) =>
           let val tmpvar = T.new_var ()
               val alist = ["S0", "S", tmpvar]
               val alist2 = [A.O "hp0", A.O "rf0"]
               val alist3 = [A.O "hp1", A.O"rf1"]
               val updexp2 = A.Minus (A.Sel(A.Rf 1, A.Reg r),
				     A.IntNum i)
	       val rf = A.Upd (A.Rf 1, A.Reg r, updexp2)
               val first =
                   if tag = ""
                   then [A.Tseq [A.Tintros alist
                               , A.Tinduction ("S0", alist2)
                               , A.Tinduction ("S", alist3)]
                       , A.TexistsS (A.Hp 1, rf)
                       , A.Tseq [A.Tsplit
                               , A.Tpara [A.Tconstructor
                                        , A.Tapply (tmpvar, [])
                        ]]]
                   else []
           in  first
           end
         | (A.Leab (i, r1, r2)) =>
           let val tmpvar = T.new_var ()
               val alist = ["S0", "S", tmpvar]
               val alist2 = [A.O "hp0", A.O "rf0"]
               val alist3 = [A.O "hp1", A.O"rf1"]
               val updexp2 = A.Plus (A.Sel(A.Rf 1, A.Reg r1),
				     A.IntNum i)
	       val rf = A.Upd (A.Rf 1, A.Reg r2, updexp2)
               val first =
                   if tag = ""
                   then [A.Tseq [A.Tintros alist
                               , A.Tinduction ("S0", alist2)
                               , A.Tinduction ("S", alist3)]
                       , A.TexistsS (A.Hp 1, rf)
                       , A.Tseq [A.Tsplit
                               , A.Tpara [A.Tconstructor
                                        , A.Tapply (tmpvar, [])
                        ]]]
                   else []
           in  first
           end
         | (A.Subr (r1, r2)) =>
           let val tmpvar = T.new_var ()
               val alist = ["S0", "S", tmpvar]
               val alist2 = [A.O "hp0", A.O "rf0"]
               val alist3 = [A.O "hp1", A.O"rf1"]
               val updexp2 = A.Minus (A.Sel (A.Rf 1, A.Reg r2),
				      A.Sel (A.Rf 1, A.Reg r1))
	       val rf = A.Upd (A.Rf 1, A.Reg r2, updexp2)
               val first =
                   if tag = ""
                   then [A.Tseq [A.Tintros alist
                               , A.Tinduction ("S0", alist2)
                               , A.Tinduction ("S", alist3)]
                       , A.TexistsS (A.Hp 1, rf)
                       , A.Tseq [A.Tsplit
                               , A.Tpara [A.Tconstructor
                                        , A.Tapply (tmpvar, [])
                        ]]]
                   else []
           in  first
           end
         | (A.Mulr (r1, r2)) =>
           let val tmpvar = T.new_var ()
               val alist = ["S0", "S", tmpvar]
               val alist2 = [A.O "hp0", A.O "rf0"]
               val alist3 = [A.O "hp1", A.O"rf1"]
               val updexp2 = A.Times (A.Sel (A.Rf 1, A.Reg r2),
				      A.Sel (A.Rf 1, A.Reg r1))
	       val rf = A.Upd (A.Rf 1, A.Reg r2, updexp2)
               val first =
                   if tag = ""
                   then [A.Tseq [A.Tintros alist
                               , A.Tinduction ("S0", alist2)
                               , A.Tinduction ("S", alist3)]
                       , A.TexistsS (A.Hp 1, rf)
                       , A.Tseq [A.Tsplit
                               , A.Tpara [A.Tconstructor
                                        , A.Tapply (tmpvar, [])
                        ]]]
                   else []
           in  first
           end
         | (A.Mulz (i, r)) =>
           let val tmpvar = T.new_var ()
               val alist = ["S0", "S", tmpvar]
               val alist2 = [A.O "hp0", A.O "rf0"]
               val alist3 = [A.O "hp1", A.O"rf1"]
               val updexp2 = A.Times (A.Sel (A.Rf 1, A.Reg r),
				      A.IntNum i)
	       val rf = A.Upd (A.Rf 1, A.Reg r, updexp2)
               val first =
                   if tag = ""
                   then [A.Tseq [A.Tintros alist
                               , A.Tinduction ("S0", alist2)
                               , A.Tinduction ("S", alist3)]
                       , A.TexistsS (A.Hp 1, rf)
                       , A.Tseq [A.Tsplit
                               , A.Tpara [A.Tconstructor
                                        , A.Tapply (tmpvar, [])
                        ]]]
                   else []
           in  first
           end
         | (A.Free r) =>
           let val tmpvar = T.new_var ()
               val alist = ["S0", "S", tmpvar]
               val alist2 = [A.O "hp0", A.O "rf0"]
               val alist3 = [A.O "hp1", A.O"rf1"]
               val rf = A.Upd(A.Rf 1, A.Reg r, A.IntNum 0)
               val first =
                   [A.Tseq [A.Tintros alist
                          , A.Tinduction ("S0", alist2)
                          , A.Tinduction ("S", alist3)]
                  , A.TexistsS (A.Hp 1, rf)
                  , A.Tseq [A.Tsplit
                          , A.Tpara [A.Tconstructor
                                   , A.Tapply (tmpvar, [])
                   ]]]
           in  first
           end
         | (A.Addz (i, r)) =>
           let val tmpvar = T.new_var ()
               val alist = ["S0", "S", tmpvar]
               val alist2 = [A.O "hp0", A.O "rf0"]
               val alist3 = [A.O "hp1", A.O"rf1"]
               val updexp2 = A.Plus (A.Sel(A.Rf 1, A.Reg r),
				     A.IntNum i)
	       val rf = A.Upd (A.Rf 1, A.Reg r, updexp2)
               val first =
                   if tag = ""
                   then [A.Tseq [A.Tintros alist
                               , A.Tinduction ("S0", alist2)
                               , A.Tinduction ("S", alist3)]
                       , A.TexistsS (A.Hp 1, rf)
                       , A.Tseq [A.Tsplit
                               , A.Tpara [A.Tconstructor
                                        , A.Tapply (tmpvar, [])
                        ]]]
                   else let val tmpvar2 = T.new_var ()
                            val tmpx = T.new_var ()
                            val tmpx1 = T.new_var ()
                            val tmpx2 = T.new_var ()
                            val tmpvar3 = T.new_var ()
                            val tmpvar4 = T.new_var ()
                            val tmpvar5 = T.new_var ()
                            val tmpvar6 = T.new_var ()
                            val tmpvar7 = T.new_var ()
                            val tmpvar8 = T.new_var ()
                            val tmpvar9 = T.new_var ()
                            val tmpvar10 = T.new_var ()

                            val tmpx3 = T.new_var ()
                            val tmpx4 = T.new_var ()
                            val alist4 = [A.L [A.O tmpvar2 
                                             , A.L [A.O tmpvar3
                                                  , A.L [A.O tmpvar4
                                                       , A.L [A.O tmpvar5
                                                            , A.L [A.O tmpvar6
                                                                 , A.L [A.O tmpvar7
                                                                      , A.L [A.O tmpvar8
                                                                           , A.L [A.O tmpvar9
                                                                                , A.O tmpvar10]]]]]]]]
                                        , A.O tmpvar]

                            val exp1 = A.Sel (A.Hp 1, 
                                              A.Plus (A.Plus (A.Sel (A.Rf 1, A.Reg A.Ebp)
                                                            , A.IntNum 4)
                                                    , A.IntNum 4))
                            val exp2 = A.Sel (A.Hp 0
                                            , A.Plus (A.Sel (A.Rf 0, A.Reg A.Esp)
                                                    , A.IntNum 4))
                            val exp3 = A.Sel (A.Hp 1
                                            , A.Plus (A.Sel (A.Rf 1, A.Reg A.Ebp)
                                                    , A.IntNum 4))
                            val exp4 = A.Sel (A.Hp 0
                                            , A.Sel (A.Rf 0, A.Reg A.Esp))
                            val exp5 = A.Plus (A.Sel (A.Rf 1, A.Reg A.Esp)
                                             , A.IntNum i)
                            val exp5' = A.Plus (exp5, A.IntNum 4)
                            val exp5'' = A.Plus (exp5', A.IntNum 4)
                            val exp6 = A.Minus (A.Sel (A.Rf 1, A.Reg A.Ebp)
                                              , A.IntNum 4)
                            val exp6' = A.Minus (exp6, A.IntNum 4)
                            val exp6'' = A.Minus (exp6', A.IntNum 4)
                            val common = [A.Tintros alist
                                        , A.Tcut (precond2 ^ " S0 S")
                                        , A.Tintros [tmpvar2]
                                        , A.Tseq [A.Tinduction ("S0", alist2)
                                                , A.Tinduction ("S", alist3)]
                                        , A.TexistsS (A.Hp 1, rf)
                                        , A.Tsplit
                                        , A.Tconstructor
                                        , A.Tapply (tmpvar2, [])
                                        , A.Tseq [A.Tinduction ("S0", alist2)
                                                , A.Tinduction ("S", alist3)]
                                        , A.Tsimpl

                                        , A.Tdestruct (tmpvar, alist4)

                                        , A.Texists "(readR rf0 edi)"
                                        , A.Tsplit
                                        , A.Treplace (exp5, exp6'')
                                        , A.Tapply (tmpvar8, [])
                                        , A.Tomega

                                        , A.Texists "(readR rf0 esi)"
                                        , A.Tsplit
                                        , A.Treplace (exp5', exp6')
                                        , A.Tapply (tmpvar7, [])
                                        , A.Tomega

                                        , A.Texists "(readR rf0 ebx)"
                                        , A.Tsplit
                                        , A.Treplace (exp5'', exp6)
                                        , A.Tapply (tmpvar6, [])
                                        , A.Tomega


                                        , A.Texists "(readR rf0 ebp)"
                                        , A.Tsplit
                                        , A.Tapply (tmpvar5, [])

                                        , A.Tseq [A.TtacIn (A.Tunfold "Stack", tmpvar2)
                                                , A.TtacIn (A.Tunfold "getrval", tmpvar2)
                                                , A.TtacIn (A.Tunfold "getmval", tmpvar2)]
                                        , A.Tseq [A.Tunfold "Stack"
                                                , A.Tunfold "getrval"
                                                , A.Tunfold "getmval"]
                                        , A.Tsplit
                                        , A.Tsplit
                                        , A.Tseq [A.Tsplit
                                                , A.Tpara [A.Tapply (tmpvar2, [])
                                                         , A.Tseq [A.Tsplit
                                                                 , A.Tpara [A.Treflexivity
                                                                          , A.Tomega]]]]
                                        , A.Tapply (tmpvar, [])]

                            val postpf = if tag = "main_ret"
                                         then [A.Tseq [A.Tsplit
                                                     , A.Tpara [A.Tomega
                                                              , A.Tseq [A.Tsplit
                                                                      , A.Tpara [A.Tomega
                                                                               , A.Tapply (tmpvar2, [])]]]]]
                                         else [ A.Tsplit
                                              , A.Tdestruct (tmpvar3, [A.O tmpx4, A.O tmpvar3])
                                              , A.Tdestruct (tmpvar4, [A.O tmpx3, A.O tmpvar4]) 
                                              , A.Texists tmpx3
                                              , A.Texists tmpx4

                                              , A.Tsplit
                                              , A.Treplace (exp1, exp2)
                                              , A.Tapply (tmpvar4, [])
                                              , A.Trewrite tmpvar9
                                              , A.Tapply (tmpvar2, [])
                                              , A.Tomega

                                              , A.Treplace (exp3, exp4)
                                              , A.Tapply (tmpvar3, [])
                                              , A.Trewrite tmpvar9
                                              , A.Tapply (tmpvar2, [])
                                              , A.Tomega

                                              , A.Tsplit
                                              , A.Trewrite tmpvar9
                                              , A.Tomega

                                              , A.Tsplit
                                              , A.Treflexivity
                                              , A.Tapply (tmpvar2, [])]
                        in  common @ postpf
                        end
           in  first
           end
         | (A.Cmpr(r1, r2)) => 
           let val tmpvar = T.new_var ()
               val alist = ["S0", "S", tmpvar]
               val alist2 = [A.O "hp0", A.O "rf0"]
               val alist3 = [A.O "hp1", A.O"rf1"]
	       val tmpassert = T.new_var ()
	       val assert1 = A.Or(A.Eq(A.Sel(A.Rf 1, A.Reg r2), A.Sel(A.Rf 1, A.Reg r1))
				, A.Or(A.Lt(A.Sel(A.Rf 1, A.Reg r2), A.Sel(A.Rf 1, A.Reg r1))
				     , A.Gt(A.Sel(A.Rf 1, A.Reg r2), A.Sel(A.Rf 1, A.Reg r1))))
	       val alist4 = A.P [A.O(tmpassert), A.L [ A.P[A.O(tmpassert), A.O(tmpassert)]]]
	       
	       val rs1' = A.Upd(A.Rf 1, A.Zf, A.IntNum 1)
	       val state1 = (A.Hp 1, A.Upd(rs1', A.Sf, A.IntNum 0))

	       val rs2' = A.Upd(A.Rf 1, A.Zf, A.IntNum 0)
	       val state2 = (A.Hp 1, A.Upd(rs2', A.Sf, A.IntNum 1))

	       val rs3' = A.Upd(A.Rf 1, A.Zf, A.IntNum 0)
	       val state3 = (A.Hp 1, A.Upd(rs3', A.Sf, A.IntNum 0))

               val tmpvar1 = T.new_var ()
	       val tmpvar2 = T.new_var ()
               val alist5 = [A.O tmpvar, A.L [A.O tmpvar1, A.O tmpvar2]]

               val first = [A.Tseq [A.Tintros alist
                                  , A.Tinduction ("S0", alist2)
                                  , A.Tinduction ("S", alist3)]
			  , A.Tassert(tmpassert, assert1)
			  , A.Tomega
			  , A.Tdestruct(tmpassert, [alist4])
			  , A.TexistsS state1
			  , A.Tsplit
			  , A.Tconstructor
			  , A.Tapply (tmpassert, [])
			  , A.Tdestruct(tmpvar, alist5)
			  , A.Tapply (tmpvar, [])
			  , A.Tapply (tmpassert, [])

			  , A.TexistsS state2
			  , A.Tsplit
			  , A.Tconstructor
			  , A.Tapply (tmpassert, [])
			  , A.Tdestruct(tmpvar, alist5)
			  , A.Tapply (tmpvar2, [])
			  , A.Tapply (tmpassert, [])

			  , A.TexistsS state3
			  , A.Tsplit
			  , A.Tconstructor
			  , A.Tapply (tmpassert, [])
			  , A.Tdestruct(tmpvar, alist5)
			  , A.Tapply (tmpvar1, [])
			  , A.Tapply (tmpassert, [])]
           in  first
           end
	 | (A.Cmpz(imm, r1)) =>
           let val tmpvar = T.new_var ()
               val alist = ["S0", "S", tmpvar]
               val alist2 = [A.O "hp0", A.O "rf0"]
               val alist3 = [A.O "hp1", A.O"rf1"]
	       val tmpassert = T.new_var ()
	       val assert1 = A.Or(A.Eq(A.Sel(A.Rf 1, A.Reg r1), A.IntNum(imm))
				, A.Or(A.Lt(A.Sel(A.Rf 1, A.Reg r1), A.IntNum(imm))
				     , A.Gt(A.Sel(A.Rf 1, A.Reg r1), A.IntNum(imm))))
	       val alist4 = A.P [A.O(tmpassert), A.L [ A.P[A.O(tmpassert), A.O(tmpassert)]]]
	       
	       val rs1' = A.Upd(A.Rf 1, A.Zf, A.IntNum 1)
	       val state1 = (A.Hp 1, A.Upd(rs1', A.Sf, A.IntNum 0))

	       val rs2' = A.Upd(A.Rf 1, A.Zf, A.IntNum 0)
	       val state2 = (A.Hp 1, A.Upd(rs2', A.Sf, A.IntNum 1))

	       val rs3' = A.Upd(A.Rf 1, A.Zf, A.IntNum 0)
	       val state3 = (A.Hp 1, A.Upd(rs3', A.Sf, A.IntNum 0))

               val tmpvar1 = T.new_var ()
	       val tmpvar2 = T.new_var ()
               val alist5 = [A.O tmpvar, A.L [A.O tmpvar1, A.O tmpvar2]]

               val first = [A.Tseq [A.Tintros alist
                                  , A.Tinduction ("S0", alist2)
                                  , A.Tinduction ("S", alist3)]
			  , A.Tassert(tmpassert, assert1)
			  , A.Tomega
			  , A.Tdestruct(tmpassert, [alist4])
			  , A.TexistsS state1
			  , A.Tsplit
			  , A.Tconstructor
			  , A.Tapply (tmpassert, [])
			  , A.Tdestruct(tmpvar, alist5)
			  , A.Tapply (tmpvar, [])
			  , A.Tapply (tmpassert, [])

			  , A.TexistsS state2
			  , A.Tsplit
			  , A.Tconstructor
			  , A.Tapply (tmpassert, [])
			  , A.Tdestruct(tmpvar, alist5)
			  , A.Tapply (tmpvar2, [])
			  , A.Tapply (tmpassert, [])

			  , A.TexistsS state3
			  , A.Tsplit
			  , A.Tconstructor
			  , A.Tapply (tmpassert, [])
			  , A.Tdestruct(tmpvar, alist5)
			  , A.Tapply (tmpvar1, [])
			  , A.Tapply (tmpassert, [])]
           in  first
           end
	 | _ => [])

  fun genSubpf2 (precond : string, precond2 : string, na' : string, i : A.instr, lemName : string) : A.tactic list = 
      (case i
        of (A.Movld (i, r1, r2)) =>
           let val tmpvar = T.new_var ()
               val tmpvar2 = T.new_var ()
               val tmpvar3 = T.new_var ()
               val tmpx = T.new_var ()
               val alist = ["S0", "S", tmpvar]
               val alist2 = [A.O "hp0", A.O "rf0"]
               val alist3 = [A.O "hp1", A.O"rf1"]
               val alist4 = [A.O tmpx, A.L [A.O tmpvar2, A.O tmpvar3]]
               val rf = A.Upd(A.Rf 1, A.Reg r2, A.Id tmpx)
               val first = [A.Tintros alist
                          , A.Tcut (precond2^" S0 S")
                          , A.Tintros [tmpvar2]
                          , A.Tseq [A.Tinduction ("S0", alist2)
                                  , A.Tinduction ("S", alist3)]
                          , A.Tdestruct (tmpvar2, alist4)
                          , A.TexistsS (A.Hp 1, rf)
                          , A.Tseq [A.Tsplit
                                  , A.Tpara [A.Tseq [A.Tconstructor
                                                   , A.Tapply (tmpvar2, [])]
                                           , A.Tapply (tmpvar3, [])
                                   ]]
                          , A.Tapply (lemName, [])
                          , A.Tapply (tmpvar, [])]
           in  first
           end
         | (A.Movz (i, r, t)) =>
           let val tmpvar = T.new_var ()
               val tmpvar2 = T.new_var ()
               val alist = ["S0", "S", tmpvar]
               val alist2 = [A.O "hp0", A.O "rf0"]
               val alist3 = [A.O "hp1", A.O"rf1"]
               val rf = A.Upd (A.Rf 1, A.Reg r, A.IntNum i)
               val first = [A.Tintros alist
                          , A.Tcut (precond2 ^" S0 S")
                          , A.Tintros [tmpvar2]
                          , A.Tseq [A.Tinduction ("S0", alist2)
                                  , A.Tinduction ("S", alist3)]
                          , A.TexistsS (A.Hp 1, rf)
                          , A.Tseq [A.Tsplit
                                  , A.Tpara [A.Tconstructor
                                           , A.Tapply (tmpvar2, [])
                                   ]]
                          , A.Tapply (lemName, [])
                          , A.Tapply (tmpvar, [])]
           in  first
           end
         | _ => [])


  fun genWfCbPf (fname, cb) =
      let val _ = if !localDebug
                  then print ("cb name is : "^ (A.getCbLab cb)^"\n")
                  else ()
          val (prf, ptag) = case (A.getCbPf cb)
                             of  NONE => raise Fail "no proof at all"
                               | SOME p => p
          val lab = A.getCbLab cb
          val _ = dbpr (lab ^"'s tag = "^ ptag^"\n")
          val precondName = cbTpPrefix ^ (filtDot lab)
          val (precond2Name', precond2a) = if ptag = ""
                                           then ("", fn s0 =>fn s => A.True) 
                                           else (A.getCbFstA cb)
          val precond2Name = (filtDot precond2Name')
          val fstPremiseName = cbFstPremiseName
          val cbName = cbPrefix ^ (filtDot lab)
          val fctName = fname ^ fctPostfix
          val sgName = signame
          val prolog = [A.Tproof, A.Tintros [fstPremiseName], A.Tunfold cbName]
          val epilog = [A.Tqed]
          val _ = T.reset_var ()
          fun gen (precond, precond2, pf, tag) =
              case pf 
               of A.WfSeq (subpf, na', is) => 
                  let val _ = if !localDebug
                              then print "I_SEQ\n"
                              else ()
                      val subpf1 = [A.Tapply (fstPremiseName, [])]
                      val subpf2 = gen (na', "", subpf, "")
                      val subpf3 = 
                          if tag = "" orelse tag = fname orelse tag = (fname^"_ret")
                          then let val i = 
                                       (case is
                                         of  (i' :: is') => i'
                                           | [] => raise Fail "code block should not be empty")
                               in  genSubpf (precond, precond2, na', i, tag)
                               end
                          else let val lemName = lemmaPrefix ^ (filtDot tag)
                                   val i = 
                                       (case is
                                         of  (i' :: is') => i'
                                           | [] => raise Fail "code block should not be empty")  
                               in  genSubpf2 (precond, precond2, na', i, lemName)
                               end 
                      val alist1 = [("fct", fctName), ("p'", na')] 
                      val first = [A.Tapply ("I_SEQ", alist1)]
                      val _ = if !localDebug
                              then print "I_SEQ\tend\n"
                              else ()
                  in  first @ subpf1 @ subpf2 @ subpf3
                  end
                | A.WfJmp (na', instr) => 
                  let val _ = if !localDebug
                              then print "I_JMP\n"
                              else ()
                      val alist1 = [("fct", fctName)]
                      val first = [A.Tapply ("I_JMP", alist1)]
                      val subpf1 = if tag = ""
                                   then let val tmpVar = T.new_var()
                                            val alist2 = ["S0", "S", tmpVar]
                                            val alist3 = [A.O "hp1", A.O "rf1"]
                                            val alist4 = [A.O "hp0", A.O"rf0"]
                                        in  [A.Tintros alist2
                                           , A.Texists na'
                                           , A.Tsplit
                                           , A.Tapply (fstPremiseName, [])
                                           , A.Tsplit
                                           , A.Tseq [A.Tunfold fctName
                                                   , A.Trepeat (A.Tseq [A.Tconstructor, (A.Ttry A.Tomega)])]
                                           , A.Tseq [A.Tinduction ("S", alist3), A.Tinduction ("S0", alist4)]
                                           , A.Tapply (tmpVar, [])
                                            ]
                                        end
                                   else let val tmpVar = T.new_var()
                                            val tmpvar2 = T.new_var ()
                                            val alist2 = ["S0", "S", tmpVar]
                                            val lemName = lemmaPrefix ^ (filtDot tag) 
                                        in  [A.Tintros alist2
                                           , A.Texists na'
                                           , A.Tsplit
                                           , A.Tapply (fstPremiseName, [])
                                           , A.Tsplit
                                           , A.Tseq [A.Tunfold fctName
                                                   , A.Trepeat (A.Tseq [A.Tconstructor, (A.Ttry A.Tomega)])]
                                           , A.Tcut (precond2^ " S0 S")
                                           , A.Tintros [tmpvar2]
                                           , A.Tapply (tmpvar2, [])
                                           , A.Tapply (lemName, [])
                                           , A.Tapply (tmpVar, [])]
                                        end            
                      val _ = if !localDebug
                              then print "I_JMP\tend\n"
                              else ()                                        
                  in  first @ subpf1
                  end
                 
                | A.WfJe (na', nan', instr) =>
                  let val _ = if !localDebug
                              then print "I_JE\n"
                              else ()
                      val alist1 = [("fct", fctName)]
                      val first = [A.Tapply ("I_JE", alist1)]
                      val subpf1 = 
                          if tag = ""
                          then let val tmpVar = T.new_var()
                                   val alist2 = ["S0", "S", tmpVar]
                                   val tmpVar1 = T.new_var ()
                                   val alist3 = [tmpVar1]
                                   val tmpVar2 = T.new_var ()
                                   val tmpVar3 = T.new_var ()
                                   val alist4 = [A.O tmpVar2, A.O tmpVar3]
                                   val alist5 = [A.O "hp1", A.O "rf1"]
                                   val alist6 = [A.O "hp0", A.O"rf0"]
                               in  [A.Tseq [ A.Tintros alist2
					   , A.Tinduction ("S0", alist6)
					   , A.Tinduction ("S", alist5)]
				  , A.Tunfold ("getfrval")

				  , A.TtacIn (A.Tunfold(precond), tmpVar)

				  , A.Tdestruct (tmpVar, alist4)
				  , A.Tsplit

				  , A.Tintros alist3
				  , A.Texists na'
				  , A.Tsplit
				  , A.Tapply (fstPremiseName, [])
				  , A.Tsplit
				  , A.Tunfold (fctName)
				  , A.Trepeat (A.Tseq [A.Tconstructor, (A.Ttry A.Tomega)])

				  , A.Tunfold na'

				  , A.Tapply (tmpVar2, []) 
				  , A.Tapply (tmpVar1, [])

				  , A.Tintros alist3
				  , A.Texists nan'
				  , A.Tsplit
				  , A.Tapply (fstPremiseName, [])
				  , A.Tsplit
				  , A.Tunfold (fctName)
				  , A.Trepeat (A.Tseq [A.Tconstructor, (A.Ttry A.Tomega)])

				  , A.Tunfold nan'

				  , A.Tapply (tmpVar3, [])
				  , A.Tapply (tmpVar1, [])]
                               end
                          else let val lemName = lemmaPrefix ^ (filtDot tag) 
                               in  [A.Tapply (lemName, [])]
                               end 
                  in  first @ subpf1
                  end
                | A.WfJg (na', nan', instr) => 
                  let val _ = if !localDebug
                              then print "I_JG\n"
                              else ()
                      val alist1 = [("fct", fctName)]
                      val first = [A.Tapply ("I_JG", alist1)]
                      val subpf1 = 
                          if tag = ""
                          then let val tmpVar = T.new_var()
                                   val alist2 = ["S0", "S", tmpVar]
                                   val tmpVar1 = T.new_var ()
                                   val alist3 = [tmpVar1]
                                   val tmpVar2 = T.new_var ()
                                   val tmpVar3 = T.new_var ()
                                   val alist4 = [A.O tmpVar2, A.O tmpVar3]
                                   val alist5 = [A.O "hp1", A.O "rf1"]
                                   val alist6 = [A.O "hp0", A.O"rf0"]
                               in  [A.Tseq [ A.Tintros alist2
					   , A.Tinduction ("S0", alist6)
					   , A.Tinduction ("S", alist5)]
				  , A.Tunfold ("getfrval")

				  , A.TtacIn (A.Tunfold(precond), tmpVar)

				  , A.Tdestruct (tmpVar, alist4)
				  , A.Tsplit

				  , A.Tintros alist3
				  , A.Texists na'
				  , A.Tsplit
				  , A.Tapply (fstPremiseName, [])
				  , A.Tsplit
				  , A.Tunfold (fctName)
				  , A.Trepeat (A.Tseq [A.Tconstructor, (A.Ttry A.Tomega)])

				  , A.Tunfold na'

				  , A.Tapply (tmpVar2, []) 
				  , A.Tapply (tmpVar1, [])

				  , A.Tintros alist3
				  , A.Texists nan'
				  , A.Tsplit
				  , A.Tapply (fstPremiseName, [])
				  , A.Tsplit
				  , A.Tunfold (fctName)
				  , A.Trepeat (A.Tseq [A.Tconstructor, (A.Ttry A.Tomega)])

				  , A.Tunfold nan'

				  , A.Tapply (tmpVar3, [])
				  , A.Tapply (tmpVar1, [])]
                               end
                          else let val lemName = lemmaPrefix ^ (filtDot tag) 
                               in  [A.Tapply (lemName, [])]
                               end 
                  in  first @ subpf1
                  end
                | A.WfJge (na', nan', instr) => 
                  let val _ = if !localDebug
                              then print "I_JGE\n"
                              else ()
                      val alist1 = [("fct", fctName)]
                      val first = [A.Tapply ("I_JGE", alist1)]
                      val subpf1 = 
                          if tag = ""
                          then let val tmpVar = T.new_var()
                                   val alist2 = ["S0", "S", tmpVar]
                                   val tmpVar1 = T.new_var ()
                                   val alist3 = [tmpVar1]
                                   val tmpVar2 = T.new_var ()
                                   val tmpVar3 = T.new_var ()
                                   val alist4 = [A.O tmpVar2, A.O tmpVar3]
                                   val alist5 = [A.O "hp1", A.O "rf1"]
                                   val alist6 = [A.O "hp0", A.O"rf0"]
                               in  [A.Tseq [ A.Tintros alist2
					   , A.Tinduction ("S0", alist6)
					   , A.Tinduction ("S", alist5)]
				  , A.Tunfold ("getfrval")

				  , A.TtacIn (A.Tunfold(precond), tmpVar)

				  , A.Tdestruct (tmpVar, alist4)
				  , A.Tsplit

				  , A.Tintros alist3
				  , A.Texists na'
				  , A.Tsplit
				  , A.Tapply (fstPremiseName, [])
				  , A.Tsplit
				  , A.Tunfold (fctName)
				  , A.Trepeat (A.Tseq [A.Tconstructor, (A.Ttry A.Tomega)])

				  , A.Tunfold na'

				  , A.Tapply (tmpVar2, []) 
				  , A.Tapply (tmpVar1, [])

				  , A.Tintros alist3
				  , A.Texists nan'
				  , A.Tsplit
				  , A.Tapply (fstPremiseName, [])
				  , A.Tsplit
				  , A.Tunfold (fctName)
				  , A.Trepeat (A.Tseq [A.Tconstructor, (A.Ttry A.Tomega)])

				  , A.Tunfold nan'

				  , A.Tapply (tmpVar3, [])
				  , A.Tapply (tmpVar1, [])]
                               end
                          else let val lemName = lemmaPrefix ^ (filtDot tag) 
                               in  [A.Tapply (lemName, [])]
                               end 
                  in  first @ subpf1
                  end
                | A.WfCall (na', nan', instr) => 
                  let val _ = if !localDebug
                              then print "I_CALL\n"
                              else ()
                      val (pname, qname) = (case instr
                                             of A.Call (f, fret) => (preCondPrefix^(filtDot f),postCondPrefix ^(filtDot f))
                                              | _ => raise Fail "The instruction should be call.")
                      val alist1 = [("fct", fctName), ("pf", pname), ("qf", qname), ("p'", nan')]
                      val tmpvar = T.new_var ()
                      val tmpvar1 = T.new_var ()
                      val tmpvar2 = T.new_var ()
                      val alist2 = [A.O "hp0", A.O"rf0"]
                      val alist3 = [A.O "hp1", A.O"rf1"]
                      val alist5 = [A.O "hp3", A.O"rf3"]
                      val alist4 = [A.O tmpvar, A.O tmpvar1]
                      val alist6 = [A.O tmpvar1, A.O tmpvar2]
                      val first = [A.Tapply ("I_CALL", alist1)]
                      val subpf1 = [A.Tomega]
                      val subpf2 = [A.Tapply (fstPremiseName, [])]
                      val subpf3 = [A.Tseq [A.Tunfold fctName
                                          , A.Trepeat (A.Tseq [A.Tconstructor, (A.Ttry A.Tomega)])]]
                      val subpf4 = [A.Tseq [A.Tunfold sgName
                                          , A.Trepeat (A.Tseq [A.Tconstructor, (A.Ttry A.Tomega)])]]
                      val lemName = lemmaPrefix ^ (filtDot tag)
                      val subpf5 = if tag = ""
                                   then [A.Tseq [A.Tintros ["S0", "S", tmpvar]
                                               , A.Tinduction ("S0", alist2)
                                               , A.Tinduction ("S", alist3)]

                                       , A.Tseq [A.Tunfold pname
                                               , A.Tunfold "updmval"
                                               , A.Tunfold "updrval"
                                               , A.Tunfold "getrval"]


                                       , A.Tseq [                                         
                                         A.Tdestruct (tmpvar, alist4)
                                       , A.Tapply (tmpvar, [])]]
                                   else [A.Tintros ["S0", "S", tmpvar]
                                       , A.Tcut (precond2^" S0 S")
                                       , A.Tintros [tmpvar1]
                                       , A.Tseq [A.Tinduction ("S0", alist2)
                                               , A.Tinduction ("S", alist3)]

                                       , A.Tseq [A.Tunfold pname
                                               , A.Tunfold "updmval"
                                               , A.Tunfold "updrval"
                                               , A.Tunfold "getrval"]

                                       , A.Tseq [A.Tdestruct (tmpvar1, alist6)
                                               , A.Tapply (tmpvar1, [])]
                                       , A.Tapply (lemName, [])
                                       , A.Tapply (tmpvar, [])]
                      val subpf6 = if tag = ""
                                   then [A.Tseq [A.Tintros ["S0", "S", "S'", tmpvar]
                                               , A.Tinduction ("S0", alist2)
                                               , A.Tinduction ("S", alist3)
                                               , A.Tinduction ("S'", alist5)]

                                       , A.Tseq [A.Tunfold qname
                                               , A.Tunfold "updmval"
                                               , A.Tunfold "updrval"
                                               , A.Tunfold "getrval"
                                               , A.Tunfold nan']

                                       , A.Tseq [A.Tdestruct (tmpvar, alist4)
                                               , A.Tapply (tmpvar1, [])]]
                                   else [A.Tintros ["S0", "S", "S'", tmpvar]
                                       , A.Tcut (precond2^" S0 S")
                                       , A.Tintros [tmpvar1]
                                       , A.Tseq [A.Tinduction ("S0", alist2)
                                               , A.Tinduction ("S", alist3)
                                               , A.Tinduction ("S'", alist5)]

                                       , A.Tseq [A.Tunfold qname
                                               , A.Tunfold "updmval"
                                               , A.Tunfold "updrval"
                                               , A.Tunfold "getrval"
                                               , A.Tunfold nan']

                                       , A.Tseq [A.Tdestruct (tmpvar1, alist6)
                                               , A.Tapply (tmpvar2, [])]
                                       , A.Tapply (lemName, [])
                                       , A.Tapply (tmpvar, [])] 
                  in  first @ subpf1 @ subpf2 @ subpf3 @ subpf4 @ subpf5 @ subpf6
                  end
                | A.WfMalloc (na', instr) => 
                  let val _ = if !localDebug
                              then print "I_MALLOC\n"
                              else ()
                      val alist1 = [("fct", fctName)]
                      val first = [A.Tapply ("I_MALLOC", alist1)]
                      val subpf1 = if tag = ""
                                   then let val tmpvar = T.new_var()
                                            val tmpvar2 = T.new_var ()
                                            val tmpl = T.new_var ()
                                            val alist2 = ["S0", "S", tmpvar, tmpl, tmpvar2]
                                            val alist3 = [A.O "hp1", A.O "rf1"]
                                            val alist4 = [A.O "hp0", A.O"rf0"]
                                        in  [A.Tintros alist2
                                           , A.Texists na'
                                           , A.Tsplit
                                           , A.Tapply (fstPremiseName, [])
                                           , A.Tsplit
                                           , A.Tseq [A.Tunfold fctName
                                                   , A.Trepeat (A.Tseq [A.Tconstructor, (A.Ttry A.Tomega)])]
                                           , A.Tseq [A.Tinduction ("S", alist3), A.Tinduction ("S0", alist4)]

                                           , A.Tseq [A.Tunfold na'
                                                   , A.Tunfold "updrval"
                                                   , A.Tunfold "writeSN"
                                                   , A.Tunfold "mwriteN"]

                                           , A.TtacIn (A.Tunfold precond, tmpvar)
 
                                           , A.Tapply (tmpvar, [])
                                           , A.Tapply (tmpvar2, [])]
                                        end
                                   else let val tmpvar = T.new_var() 
                                            val tmpvar2 = T.new_var ()
                                            val tmpvar3 = T.new_var ()
                                            val tmpl = T.new_var ()
                                            val alist2 = ["S0", "S", tmpvar, tmpl, tmpvar2]
                                            val alist3 = [A.O "hp1", A.O "rf1"]
                                            val alist4 = [A.O "hp0", A.O"rf0"]
                                            val lemName = lemmaPrefix ^ (filtDot tag) 
                                        in  [A.Tintros alist2
                                           , A.Texists na'
                                           , A.Tsplit
                                           , A.Tapply (fstPremiseName, [])
                                           , A.Tsplit
                                           , A.Tseq [A.Tunfold fctName
                                                   , A.Trepeat (A.Tseq [A.Tconstructor, (A.Ttry A.Tomega)])]

                                           , A.Tcut (precond2^" S0 S")
                                           , A.Tintros [tmpvar3]
                                           , A.Tseq [A.Tinduction ("S", alist3), A.Tinduction ("S0", alist4)]

                                           , A.TtacIn (A.Tunfold precond2, tmpvar3)

                                           , A.Tseq [A.Tunfold na'
                                                   , A.Tunfold "updrval"
                                                   , A.Tunfold "writeSN"
                                                   , A.Tunfold "mwriteN"]

                                           , A.Tapply (tmpvar3, [])
                                           , A.Tapply (tmpvar2, [])
                                           , A.Tapply (lemName, [])
                                           , A.Tapply (tmpvar, [])]
                                        end      
                  in  first @ subpf1
                  end
                | A.WfRet na' =>
                  if fname = "main"
                  then let val _ = if !localDebug
                                   then print "I_RET_MAIN\n"
                                   else ()
                           val fprename = preCondPrefix ^ "main"
                           val fpostname = postCondPrefix ^ "main"
                           val alist1 = [("fct", fctName), ("pf", fprename), ("qf", fpostname)]
                           val first = [A.Tapply ("I_RET_MAIN", alist1)]
                           val subpf1 = [A.Tapply (fstPremiseName, [])]
                           val subpf2 = [A.Tunfold sgName
                                       , A.Trepeat(A.Tseq [A.Tconstructor, A.Ttry (A.Tomega)])]
                           val subpf3 = let val tmpVar = T.new_var()
                                            val tmpVar2 = T.new_var ()
                                            val alist2 = ["S0", "S", tmpVar]
                                            val alist3 = [A.O "hp1", A.O "rf1"]
                                            val alist4 = [A.O "hp0", A.O"rf0"]
                                            val alist5 = [A.O tmpVar, A.O tmpVar2]
                                        in  [A.Tseq [A.Tintros alist2
                                                   , A.Tinduction ("S0", alist4)
                                                   , A.Tinduction ("S", alist3)]
                                           , A.Tseq [A.Tdestruct (tmpVar, alist5)
                                                   , A.Tapply (tmpVar, [])]

                                           , A.Tseq [A.Tintros alist2
                                                   , A.Tinduction ("S0", alist4)
                                                   , A.Tinduction ("S", alist3)]
                                           , A.Tseq [A.Tdestruct (tmpVar, alist5)
                                                   , A.Tapply (tmpVar2, [])]]
                                        end
                       in  first @ subpf1 @ subpf2 @ subpf3
                       end
                  else let val _ = if !localDebug
                                   then print "I_RET\n"
                                   else ()
                           val fprename = preCondPrefix ^ (filtDot fname)
                           val fpostname = postCondPrefix ^ (filtDot fname)
                           val alist1 = [("fct", fctName), ("pf", fprename), ("qf", fpostname)]
                           val first = [A.Tapply ("I_RET", alist1)]
                           val subpf1 = [A.Tapply (fstPremiseName, [])]
                           val subpf2 = [A.Tunfold sgName
                                       , A.Trepeat(A.Tseq [A.Tconstructor, A.Ttry (A.Tomega)])]
                           val subpf3 = let val tmpVar = T.new_var()
                                            val tmpVar2 = T.new_var ()
                                            val alist2 = ["S0", "S", tmpVar]
                                            val alist3 = [A.O "hp1", A.O "rf1"]
                                            val alist4 = [A.O "hp0", A.O"rf0"]
                                            val alist5 = [A.O tmpVar, A.O tmpVar2]
                                        in  [A.Tseq [A.Tintros alist2
                                                   , A.Tinduction ("S0", alist4)
                                                   , A.Tinduction ("S", alist3)]
                                           , A.Tseq [A.Tdestruct (tmpVar, alist5)
                                                   , A.Tapply (tmpVar, [])]

                                           , A.Tseq [A.Tintros alist2
                                                   , A.Tinduction ("S0", alist4)
                                                   , A.Tinduction ("S", alist3)]
                                           , A.Tseq [A.Tdestruct (tmpVar, alist5)
                                                   , A.Tapply (tmpVar2, [])]]
                                        end
                           val subpf4 = [A.Tomega]            
                           val _ = if !localDebug
                                   then print "I_JMP\tend\n"
                                   else ()                                        
                       in  first @ subpf1 @ subpf2 @ subpf3 @ subpf4
                       end
          val all = prolog @ (gen (precondName, precond2Name,  prf, ptag)) @ epilog
          val _ = if !localDebug
                  then print ("cb : "^ (A.getCbLab cb)^"'s proof generated\n")
                  else ()
          val retv =  String.concat (List.map (Coq.ppTactic) all)
          val _ = if !localDebug
                  then print ("cb : "^ (A.getCbLab cb)^" finished\n")
                  else ()
      in  retv
      end 



  fun genWfCb (fname, cb) = 
      let val lem = genWfCbLem (fname, cb)
          val prf = genWfCbPf (fname, cb)
      in  lem ^ prf
      end

  fun genWfFblk frame = 
      let val codelist = 
              getSomethingFromFrame (frame, F.getCode, "no code, impossible")
	  val fname = F.getFname frame
	  val lablist = List.map (fn t => filtDot(A.getCbLab t)) codelist

	  val lem = 
	      "Lemma "^wfFblkPrefix^fname^" :\n"^"WF_FBLK "^ctname^" "^fname^" "
	      ^signame^" "^fname^fctPostfix^" "^fname^fchPostfix^".\n"

	  val prftac1 = List.foldl (fn (t, r) => let val t' = [A.Tapply("wf_fb_cons", [])
							     , A.Tapply(ctname, [])
							     , A.Tapply(signame, [])
							     , A.Tapply(cbLemName(t), [])
							     , A.Tseq[A.Tunfold ctname
								    , A.Tunfold (fname^fctPostfix)]
							     , A.Trepeat (A.Tseq [A.Tconstructor, (A.Ttry A.Tomega)])]
						 in t'@r
						 end)
			[A.Tapply("wf_fb_emp", [])
		       , A.Tqed] lablist

	  val prftac = [A.Tproof
		      , A.Tconstructor
		      , A.Tseq[A.Tunfold(ctname)
			     , A.Tunfold(fname^fctPostfix)]
		      , A.Trepeat (A.Tseq [A.Tconstructor, (A.Ttry A.Tomega)])
		      , A.Tseq[A.Tunfold(fname^fctPostfix)
			     , A.Tunfold(fname^fchPostfix)]]
	  val tac = String.concat (List.map (Coq.ppTactic) (prftac@prftac1))
      in lem^tac
      end

  fun mkfilename (origin, postfix, dir) = 
      let val slist = String.tokens (fn c => (c = #"/") orelse (c = #"\\")) origin
          val file = "coq_"^(filtDot (List.hd (List.rev slist)))
      in  dir ^ file ^ postfix
      end 
  
  val depFiles : string list ref = ref []

  fun genWfFun frame = 
      let val codelist =
              getSomethingFromFrame (frame, F.getCode, "no code, impossible")
          val fname = F.getFname frame
	  val fnameHd = mkfilename(File.nameToString (!Err.file), "", "")
	  val dirname = "fcap/"
	  val epiname = filtDot(F.getEpilog frame)

          val _ = dbpr "genWfFun 1"
          fun f cb = 
	      let val prfStr = genWfCb (fname, cb)
		  val cbStr = filtDot(A.getCbLab cb)

		  val mreqstr3 = "Require Import common.\n"^
				 "Require Import zutil.\n"^
				 "Require Import regfile.\n"^
				 "Require Import memory.\n"^
				 "Require Import fcap.\n"^
				 "Require Import lemma.\n"^
				 "Require Import rules.\n"^
				 "Require Import ZArith.\n"^
				 "Require Import "^fnameHd^"Def.\n"^
				 "Require Import "^fnameHd^"Cht.\n"^
				 "Open Local Scope Z_scope.\n\n"
		  val mfile3 = dirname^fnameHd^cbStr^"Lab.v"
		  val _ = depFiles := (fnameHd^cbStr^"Lab.v")::(!depFiles)
		  val mcoqstr3 = mreqstr3 ^ prfStr
                  val coqfile3 = File.creat mfile3
	      in  File.write (coqfile3, mcoqstr3)
	      end
          fun g cb = 
              let val (pf, tag) = case A.getCbPf cb
                                   of  NONE => raise Fail "why no proof?"
                                     | SOME a => a
              in  dbpr ((A.getCbLab cb) ^ " tag = "^tag^"\n")
              end
          val _ = if !localDebug
                  then (List.map g (List.rev codelist); ())
                  else ()
          val _ = List.map f (List.rev codelist)

	  val strWF = "\n\n"^(genWfFblk frame)^"\n"

	  val lem = 
	      "Lemma "^wfFuncPrefix^fname^" :\n"^
	      "WF_FUNC "^ctname^" "^signame^" "^fname^fchPostfix^" "^
	      fname^fctPostfix^" "^fname^
	      " (fnspec "^preCondPrefix^fname^" "^postCondPrefix^fname^").\n"
	  val tac = [A.Tproof
		   , A.Tapply ("wf_f", [("p0", cbTpPrefix^fname), ("is", cbPrefix^epiname)])
		   , A.Tapply (wfFblkPrefix^fname, [])
		   , A.Tunfold signame
		   , A.Trepeat (A.Tseq [A.Tconstructor, (A.Ttry A.Tomega)])
		   , A.Tunfold (fname^fctPostfix)
		   , A.Trepeat (A.Tseq [A.Tconstructor, (A.Ttry A.Tomega)])
		   , A.Texists epiname
		   , A.Tsplit
		   , A.Tunfold (fname^fchPostfix)
		   , A.Trepeat (A.Tseq [A.Tconstructor, (A.Ttry A.Tomega)])
		   , A.Tseq [A.Tunfold (cbPrefix^epiname)
			   , A.Tsimpl
			   , A.Tauto] (* no trivial tactic *)
		   , A.Tintros ["S", "H"]
		   , A.TtacIn(A.Tunfold(preCondPrefix^fname), "H")
		   , A.Tunfold(cbTpPrefix^fname)
		   , A.Tapply("H", [])
		   , A.Tqed]
	  val tacstr = String.concat (List.map (Coq.ppTactic) tac)
	  val strFunc = "\n"^lem^tacstr^"\n"

	  (* output to file *)
	  val mreqstr4 = "Require Import common.\n"^
			 "Require Import zutil.\n"^
			 "Require Import regfile.\n"^
			 "Require Import memory.\n"^
			 "Require Import fcap.\n"^
			 "Require Import lemma.\n"^
			 "Require Import rules.\n"^
			 "Require Import ZArith.\n"^
			 "Require Import "^fnameHd^"Def.\n"^
			 "Require Import "^fnameHd^"Cht.\n"^
			 (String.concat(List.map (fn t => let val t' = filtDot(A.getCbLab t)
							  in "Require Import "^fnameHd^t'^"Lab.\n"
							  end) codelist))^
			 "Open Local Scope Z_scope.\n\n"
	  val mfile4 = dirname^fnameHd^fname^"Fun.v"
	  val mcoqstr4 = mreqstr4 ^ strWF^strFunc
          fun tryfun () = TextIO.openOut (mfile4)
              handle Io => (print ("cannot create file "^mfile4^"\n")
                          ; raise Fail "")
	  val coqfile4 = tryfun()
	  val _ = TextIO.output(coqfile4, mcoqstr4)
	  val _ = TextIO.closeOut(coqfile4)

      in  ()
      end

  fun genWfCh framelist =
      let val flist = List.rev (List.map F.getFname framelist)
          val lem = "Lemma "^wfCH^" : \n"^
                    "WF_CH "^ ctname ^" "^signame^" "^chname^".\n"
          val first = [A.Tproof
                     , A.Tapply ("wf_c", [])
                     , A.Tseq [A.Tunfold ctname
                             , A.Tunfold chname]]
          val last = [A.Tapply ("link_lemma", [])
                    , A.Tqed]
          fun gen ls = 
              (case ls
                of [] => [A.Tapply ("wf_c_emp", [])]
                 | (x :: xs) => 
                   let val fname = x
                       val a = "(fnspec "^preCondPrefix^fname^" "^postCondPrefix^fname^")"
                       val wff = wfFuncPrefix^fname
                       val head = [A.Tapply ("wf_c_cons", [("a", a)])]
                       val subpf1 = [A.Tseq [A.Tunfold signame
                                           , A.Trepeat (A.Tseq [A.Tconstructor
                                                              , A.Ttry A.Tomega])]]
                       val subpf2 = [A.Tapply (wff, [])]
                       val subpf3 = gen xs 
                   in  head @ subpf1 @ subpf2 @ subpf3
                   end)
          val body = gen flist
          val tac = first @ body @ last
          val tacstr = String.concat (List.map (Coq.ppTactic) tac)  
      in  lem^tacstr
      end

  fun genWfProg framel = (* WIP *)
      let val _ = List.map genWfFun framel
          val prgstr = genWfCh framel
      in prgstr
      end

  fun genDataLab data =
      let fun f [] = []
            | f ((A.Label (id, opta)) :: l) = (id, A.getLabId opta) :: f l
            | f (_ :: l) = f l
          val sl = f data
          val labstr = String.concat (List.map Coq.ppLab sl)
      in  "\n(* data label notation *)\n" ^ labstr ^ "\n"
      end
 
  fun genAux framelist = 
      let fun mpBKFn bk =
	      let val bklab = A.getCbLab bk
		  val bkpf = (fn NONE => raise Fail "No Proof\n"
			       | SOME(dm1, tag) => tag) (A.getCbPf bk)
	      in if bkpf = ""
		 then ""
		 else (let val (bkAhd, bkAsst) = A.getCbFstA bk 
		       in "Lemma lemma_"^(filtDot bkpf)^": forall S0 S, ("^
			  cbTpPrefix^(filtDot bklab)^" S0 S) -> ("^(filtDot bkAhd)^" S0 S).\nAdmitted.\n"
		       end)
	      end

	  fun mpFRFn fr = 
	      let val cdbks = getSomethingFromFrame (fr, F.getCode, "no code")
	      in String.concat(List.map mpBKFn cdbks)
	      end
      in String.concat(List.map mpFRFn framelist)
      end

  fun outChs (framelist, data) filename = 
      let val fnameHd = mkfilename(filename, "", "")
	  val dirname = "fcap/"
	  val mfile1 = dirname^fnameHd^"Def.v"

	  val newfl = framelist
          val dstr = genDataLab data
          val labstr = genLab newfl
          val chstr = genCodeHeap newfl

	  val mreqstr1 = "Require Import common.\n"^
			 "Require Import zutil.\n"^
			 "Require Import regfile.\n"^
			 "Require Import memory.\n"^
			 "Require Import fcap.\n"^
			 "Open Local Scope Z_scope.\n\n"

	  val mcoqstr1 = mreqstr1 ^ dstr ^ labstr ^ chstr
	  fun try () = TextIO.openOut (mfile1)
              handle Io => (print ("cannot create file "^mfile1^"\n")
                          ; raise Fail "")
          val coqfile1 = try ()
      in TextIO.output(coqfile1, mcoqstr1);
	 TextIO.closeOut(coqfile1)
      end

  fun top (framelist, data) =
      let val _ = depFiles := []
	  val newfl = justifyAsst framelist
          val _ = dbpr "top1"
          val newf2 = genProgPf newfl
          fun f fl =
              let val frame = List.hd fl
                  val lab = ".L_33_3"
                  val codelist = getSomethingFromFrame (frame, F.getCode, "no code")
                  val cb = getCode (lab, codelist)
                  val name = cbTpPrefix ^ (filtDot lab)
                  val astr = case A.getCbAsst cb
                              of  NONE => raise Fail "no assertion"
                                | SOME a => Coq.ppAsst (name, a)
              in  dbpr ("Current assertion in "^lab^" : ")
                ; dbpr astr
              end 
          val _ = dbpr "top2"
          val ctstr = genCodeHeapType newf2
          val pfstr = genWfProg newf2
	  val coqstr1 = genAux newf2
	  val _ = outChs (newfl, data) (File.nameToString (!Err.file))

	  val fnameHd = mkfilename(File.nameToString (!Err.file), "", "")
	  val dirname = "fcap/"
	  val mreqstr2 = "Require Import common.\n"^
			 "Require Import zutil.\n"^
			 "Require Import regfile.\n"^
			 "Require Import memory.\n"^
			 "Require Import fcap.\n"^
			 "Require Import lemma.\n"^
			 "Require Import rules.\n"^
			 "Require Import ZArith.\n"^
			 "Require Import "^fnameHd^"Def.\n"^
			 "Open Local Scope Z_scope.\n\n"
	  val mfile2 = dirname^fnameHd^"Cht.v"
	  val mcoqstr2 = mreqstr2 ^ctstr ^coqstr1
          val coqfile2 = File.creat mfile2
	  val _ = File.write (coqfile2, mcoqstr2)
	  val mreqstr3 = "Require Import common.\n"^
			 "Require Import zutil.\n"^
			 "Require Import regfile.\n"^
			 "Require Import memory.\n"^
			 "Require Import fcap.\n"^
			 "Require Import lemma.\n"^
			 "Require Import rules.\n"^
			 "Require Import ZArith.\n"^
			 "Require Import "^fnameHd^"Def.\n"^
			 "Require Import "^fnameHd^"Cht.\n"^
			 (String.concat(List.map (fn t => let val t' = F.getFname t
							  in "Require Import "^fnameHd^t'^"Fun.\n"
							  end) framelist))^
			 "Open Local Scope Z_scope.\n\n"
	  val mfile3 = dirname^fnameHd^"Prf.v"
	  val mcoqstr3 = mreqstr3 ^ pfstr
	  fun try3 () = TextIO.openOut (mfile3)
              handle Io => (print ("cannot create file "^mfile3)
                          ; raise Fail "")
	  val coqfile3 = try3 ()
	  val _ = TextIO.output(coqfile3, mcoqstr3)
	  val _ = TextIO.closeOut(coqfile3)
	  val mfname1 = String.tokens (fn c => (c = #"/") orelse (c = #"\\")) (File.nameToString (!Err.file))
          val mfname2 = List.hd (List.rev mfname1)
	  val mfname = filtDot (String.substring(mfname2, 0, String.size(mfname2)-2))
	  val depstr = String.concat(List.map (fn t => t^" ") (!depFiles))
	  val depfname = dirname^"dep"^mfname
	  val depfile = File.creat depfname
	  val _ = File.write (depfile, depstr)
	  val makestr = "COQC = coqc \n\n"^
			"FILEHDER = coq_\n\n"^
			"FILEDEF = _cDef\n"^
			"FILECHT = _cCht\n"^
			"FILEPRF = _cPrf\n"^
			"IN_FILE = .v\n"^
			"OUT_FILE = .vo\n"^
			"FILENAMES = "^ mfname ^"\n"^
			"OBJECT = $(addsuffix .vo,$(FILENAMES))\n"^
			"TOBJECT = $(addsuffix .tvo,$(FILENAMES))\n"^
			"all : $(OBJECT)\n"^
			"TC : $(TOBJECT)\n"^
			"%$(OUT_FILE) : \n"^
			"\t$(COQC) $(FILEHDER)$(basename $@)$(FILEDEF)$(IN_FILE)\n"^
			"\t$(COQC) $(FILEHDER)$(basename $@)$(FILECHT)$(IN_FILE)\n"^
			"\tfor i in $(shell cat dep$(basename $@)); do \\\n"^
			"\techo $$i;\\\n"^
			"\t$(COQC) $$i;\\\n"^
			"\tdone\n"^
			"\tfor i in $(wildcard coq_$(basename $@)*Fun.v); do \\\n"^
			"\techo $$i;\\\n"^
			"\t$(COQC) $$i;\\\n"^
			"\tdone\n"^
			"\t$(COQC) $(FILEHDER)$(basename $@)$(FILEPRF)$(IN_FILE)\n\n"^

			"%.tvo : \n"^
			"\ttime $(COQC) $(FILEHDER)$(basename $@)$(FILEDEF)$(IN_FILE)\n"^
			"\ttime $(COQC) $(FILEHDER)$(basename $@)$(FILECHT)$(IN_FILE)\n"^
			"\tfor i in $(shell cat dep$(basename $@)); do \\\n"^
			"\techo $$i;\\\n"^
			"\ttime $(COQC) $$i;\\\n"^
			"\tdone\n"^
			"\tfor i in $(wildcard coq_$(basename $@)*Fun.v); do \\\n"^
			"\techo $$i;\\\n"^
			"\ttime $(COQC) $$i;\\\n"^
			"\tdone\n"^
			"\ttime $(COQC) $(FILEHDER)$(basename $@)$(FILEPRF)$(IN_FILE)\n\n"^

			"clear: \n"^
			"\tfor i in $(FILENAMES); do \\\n"^
			"\trm coq_$$i*.vo;\\\n"^
			"\tdone\n"^
			"clear-src :\n"^
			"\tfor i in $(FILENAMES); do \\\n"^
			"\trm coq_$$i*.v;\\\n"^
			"\trm dep$$i;\\\n"^
			"\tdone\n"
	  val mffname = dirname^"make"^mfname
	  val coqfile4 = File.creat mffname
	  val _ = File.write (coqfile4, makestr)
      in  ()
      end
end
